「直観主義型理論（ITT, Intuitionistic Type Theory）」勉強会ノート其ノ拾六「直和の応用（途中から）」（復習編）

　こちらの復習編。

左射影

　p の依存型のときの論理読み（存在量化のとき）というのは、 の witness を取り出すということになろうかと。それがヒルベルトのアレになる。右射影だとその個体について成り立つ性質を取り出すことになる。

右射影

　左射影と同じように、規則のインスタンスであることをわかりやすくしました。

形成則について

　 や & の形成則にある、 を仮定して が出てくるというのは、具体的にどういう状況だろう？？？

導入則とラムダ抽象

　導入則の依存なしバージョンがラムダ抽象ということでよいのだろうか。

&について

　論理学の入門とかでやる自然演繹では & の と は平等だが、ITTでは非対称的である。これがおもしろい。