| 型と計算 | 命題と証明 |
|---|---|
| 型演算／構成子 | 命題結合子 |
| 依存型構成子 | 限量子 |
| 型ファミリー | (命題ファミリー) |
| インデックス域 | 論域 |
| インデックス | 個体 |
| インデックス変数 | 限量束縛変数 |
| 関数 | 保証 |
| 戻り型 | 結論命題 |
| ターゲット型 | ターゲット命題（質問の） |
| 引数リスト | コンテキスト |
| 計算可能関数 | 証明保証 |
| 計算不可能関数 | 神託保証 |
| 関数定義 | 定理記述 |
| 関数定義ヘッド | 定理ステートメント |
| 関す定義ボディ | 定理証明部 |
| 計算 | 証明 |
| 計算項 | 証明項 |
曖昧性：
矢印は明確・詳細化〈refinement〉、⇒ はカリー／ハワード／ランベック対応
- 証明 → 証明保証 ＝ 演繹圏の射 ⇒ 計算可能関数
- 証明 → 名前なし定理記述＝ステートメント＋証明項 ⇒ 無名関数定義 ＝ 関数クロージャ
- 証明 → 証明項 ⇒ 計算項
- 証明 → 定理記述の証明部 ⇒ 関数定義ボディ
- 証明 → 保証（神託含む） ⇒ 関数 （例： 記述可能な証明＝証明）
圏：
- $`{\bf Correct}`$ ： 命題と保証（神託含む）の圏
- $`{\bf Ded}`$ ： 命題と証明の圏
- $`{\bf Compute}`$ ： 計算可能関数の圏
- $`{\bf Set}`$ ： 集合と関数の圏
