まだあるの？ まだあります！
カリー／ハワード／ランベック対応〈Curry-Howard-Lambek correspondence〉は、「型理論（ラムダ計算を含む）」「論理」「圏論」の三分野のあいだの対応ですが、今回は、抽象的・一般的な圏ではなくて、集合圏と位相空間の圏を取り上げます。主に、依存型理論の概念を、論理、集合圏、位相空間の圏で何に対応するかをまとめます。
先に、幾つかの言葉の説明をしておきます。
- バンドル〈bundle〉： 多様体上のベクトル・バンドルなどとは違って、単なる連続写像 $`f:E \to B`$ のことです。全射であることも仮定しません。逆像 $`f^{-1}(b)`$ に注目します。
- 自明バンドル〈trivial bundle〉： 直積とその射影をバンドルとみなしたものです。
- 居住者〈inhabitant〉： 型理論で使われる用語で、型に所属するモノのことです。「要素」でもいいと思います。
- 論域〈domain of discourse〉： 述語論理の用語で、述語の域のことです。
- 個体〈individual〉： 論域の要素のことです。
- 具体化〈instantiation〉 ： パラメータ／インデックス／個体を特定値にして評価したモノです。
- 証拠〈witness | evidence〉 ： 原則的に証明と同義ですが、公理命題にも証拠は付いていると考えます。命題のラベルは、実際は命題の証拠の名前です。
- 背景〈background〉： 当面の興味の対象ではないが、暗黙に仮定されているものという意味で使っています。
概念・用語の対応表：
| 型理論 | 論理 | 集合圏 | 位相空間の圏 |
|---|---|---|---|
| 型 | 命題 | 集合 | 空間 |
| 計算／関数 | 証明／定理 | 写像 | 連続写像 |
| 型の居住者 | 命題の証拠 | 集合の要素 | 空間の点 |
| パラメータ付き型 | 述語／命題関数 | 集合族 | バンドル |
| パラメータの型 | 論域 | インデックス集合 | 底空間 |
| パラメータ | 個体 | インデックス | 底空間の点 |
| シグマ型 | 存在命題 | 総直和集合 | バンドルの全空間 |
| パラメータ具体化型 | 述語の個体具体化命題 | 集合族の成分集合 | バンドルのフィイバー空間 |
| - | 命題値スコーレム関数 | タプル | セクション |
| パイ型 | 全称命題 | 総直積集合 | セクション空間 |
| 一般化型判断 | 一般化シーケント | 一般化依存関数 | （底空間固定の）バンドル射 |
| 型判断 | シーケント | 依存関数 | 自明バンドルを域とするバンドル射 |
| 型コンテキスト | 前提 | 依存関数の域 | バンドル射の域である自明バンドル |
| 背景コンテキスト | 背景前提 | 依存関数の背景引数 | 自明バンドルのファイバー空間 |
| ターゲット型 | 結論命題 | 依存関数の余域 | バンドル射の余域 |
| 依存ラムダ抽象 | 全称導入 | 依存カリー化 | バンドル射のセクション空間への持ち上げ |
- ハブ記事： カリー／ハワード／ランベック対応の辞書
