型理論と論理のすり合わせ (3)

型・関数	命題・導出
0-射 型	0-射 命題
0-オペレータ 積	0-オペレータ 連言
0-オペレータ 指数	0-オペレータ 含意
0-射 指数型	0-射 含意命題
1-射 関数	1-射 導出
1-射 データ	1-射 保証〈ワランティー〉
1-射 入射〈余射影〉	1-射 証拠
1-射 射影〈成分〉	1-射 具体化
構造化型	構造化命題
複1-射 複関数	複1-射 複導出
多1-射 多関数	多1-射 多導出
ラムダ抽象	含意導入
評価写像	モーダスポネンス
0-射 パイ型	0-射 全称命題
	翻訳関手

保証〈ワランティー〉は新しく導入した言葉。

その他：

1. 型コンテキスト ＝ 構造化型
2. 関数置換 ＝ 多関数
3. 命題コンテキスト ＝ 構造化命題

ただし、役割としての型コンテキスト、命題コンテキストは使うかも。