「直観主義型理論（ITT, Intuitionistic Type Theory）」勉強会ノート其ノ拾四「デカルト積の応用（途中から）」「集合族の直和」「直和の応用（途中まで）」（復習編）

　こちらなどの復習編

コンビネータ

　コンビネータの導出は普通の命題論理の自然演繹と比較するとわかりやすいのではないかとなったので、載せときます。

だいたい同じですな。

項を隠す

　型付ラムダ計算で にあたるのは であろう。つまり、 という型を持ったなんらかの項 が存在する。この項 を suppressing したらどうなるか。「 という型が存在する」みたいな意味になりそうだが、そういう宣言に意味はあるのだろうか。論理ではこれが真理の判断になっているわけだけれど。

ApとE

　ApとEの違いがわからなかった私だが、代入操作ととらえたときに代入する側とされる側で逆になっている。Apでは型の項に代入されるが、Eでは型の項が代入されている。