「直観主義型理論（ITT, Intuitionistic Type Theory）」勉強会ノート其ノ弐拾参「有限集合」「無矛盾性」（復習編）

　こちらの復習編を簡単に。

　 であるが、 に添字がいるのかどうか、議論になった。 のケースを見ると機能していそうな感じはある。

　 除去則のオルタナティブの正当化の後半で 除去則を使えばもっと簡単だった。

型理論 (レクチャーノート／ソフトウェア学　１)