カリー／ハワード／ランベック対応〈Curry-Howard-Lambek correspondence〉は、「型理論（ラムダ計算を含む）」「論理」「圏論」の三分野の概念のあいだの精密・詳細な対応を与えてくれます。しかし、言葉はうまく対応してくれません。異なる分野の言語・文化・習慣にはギャップがあるからです。
言葉の対応表（つまり翻訳の辞書）が作れないのは僕の長年の悩みです。ことあるごとに辞書を試作してはうまくいかずヘコんでいます。
以下は、現時点でのだいたいの辞書〈対応表〉です。ハイフンの欄は適切な言葉が見つからなかった場所です。単語末尾の疑問符 '?' は、その言葉をその意味で使うことがポピュラーではないことを示します。単語末尾のアスタリスク '*' は、その言葉の意味を拡張・制限して使う必要があることを示します。
| 型理論 | 論理 | 圏論 |
|---|---|---|
| 型 | 命題 | 対象 |
| 計算 | 証明 | 射 |
| ペア型 | 連言命題 | 直積対象 |
| タグ付きユニオン型 | 選言命題 | 直和対象 |
| ユニット型 | 真命題 | 終対象 |
| ネバー型? | 偽命題 | 始対象 |
| アロー型 | 含意命題 | 指数対象〈内部ホム対象〉 |
| - | - | 図式 |
| - | - | スパン図式 |
| - | - | コスパン図式 |
| パイ型 | 全称命題 | スパン図式の極限対象 |
| シグマ型 | 存在命題 | コスパン図式の余極限対象 |
| - | - | 射達のデカルト・タプル |
| - | - | 射達の余デカルト・コタプル |
| - | - | 関手 |
| 型演算? | 結合子〈コネクティブ〉 | 圏論的コンストラクタ? |
| コンビネータ? | シーケントの推論規則 | 圏論的オペレーター? |
| 型項? | 論理式 | - |
| 計算項? | 証明項〈証明オブジェクト〉 | - |
| - | 証明可能 | - |
| 型付けコンテキスト* | 前提* | - |
| ターゲット型 | 結論命題 | 余域対象 |
| 型付け判断* | シーケント* | プロファイル?* |
| 関数定義 | 定理記述 | - |
| - | ゴール〈証明要求?〉 | - |
ハイフンの部分を無理やりに埋めてみます。当然に、見慣れない言葉が登場してしまいます。また、上の表にはない幾つかの言葉を追加します。すべてポピュラーではない言葉なので、いちいち疑問符は付けません。
| 型理論 | 論理 | 圏論 |
|---|---|---|
| 型宇宙 | 命題宇宙 | 圏の対象類 |
| （型の）要素 | （命題の）証拠 | ポインティグ射 |
| 基本型〈組み込み型〉 | 基本命題〈アトム命題〉 | 基本単純対象 |
| 基本関数〈組み込み関数〉 | 公理（命題と証拠） | 基本射 |
| 型・計算の図式 | 命題・証明の図式 | 対象・射の図式 |
| 同一コンテキストの計算族 | 同一前提の証明族 | スパン図式 |
| 同一ターゲットの計算族 | 同一結論の証明族 | コスパン図式 |
| 計算族のインデックス | パラメータ変数 | 図式のインデックス〈ラベル〉 |
| 計算達のデカルト・タプル | 証明達のデカルト・タプル | 射達のデカルト・タプル |
| 計算達の余デカルト・コタプル | 証明達の余デカルト・コタプル | 射達の余デカルト・コタプル |
| 型理論的関手 | 論理的関手 | 関手 |
| 型項 | 論理式 | 対象項 |
| 計算項 | 証明項 | 射項 |
| 可達 | 証明可能 | 可達 |
| 型付けコンテキスト | 前提 | 圏論的コンテキスト〈複域／多域〉 |
| 型のバンチ | 命題のバンチ | 対象のバンチ |
| 関数定義 | 定理記述 | 射定義 |
| 関数宣言 | 事実（の宣言） | 射のプロファイル（の宣言） |
| 生成された計算系 | セオリー | 生成された圏 |
| 計算構成要求 | 証明構成要求〈ゴール〉 | 射構成要求 |
