Per Martin-Löfの"Intuitionistic Type Theory"（1984）の勉強会の記録。他の回はこちらから。 今回は「デカルト積の応用」の節のみ。 登場する論理規則は以下の画像を参照。比較のために等号規則を除いた規則も載せた。 含意の定義 これは が に依存しない…