| 型・関数 | 命題・導出 |
|---|---|
| 0-射 型 | 0-射 命題 |
| 0-オペレータ 積 | 0-オペレータ 連言 |
| 0-オペレータ 指数 | 0-オペレータ 含意 |
| 0-射 指数型 | 0-射 含意命題 |
| 1-射 関数 | 1-射 導出 |
| 1-射 データ | 1-射 保証〈ワランティー〉 |
| 1-射 入射〈余射影〉 | 1-射 証拠 |
| 1-射 射影〈成分〉 | 1-射 具体化 |
| 構造化型 | 構造化命題 |
| 複1-射 複関数 | 複1-射 複導出 |
| 多1-射 多関数 | 多1-射 多導出 |
| ラムダ抽象 | 含意導入 |
| 評価写像 | モーダスポネンス |
| 0-射 パイ型 | 0-射 全称命題 |
| 翻訳関手 |
保証〈ワランティー〉は新しく導入した言葉。
その他：
- 型コンテキスト ＝ 構造化型
- 関数置換 ＝ 多関数
- 命題コンテキスト ＝ 構造化命題
ただし、役割としての型コンテキスト、命題コンテキストは使うかも。
