曇りなき眼で見定めブログ

学生です。勉強したことを書いていく所存です。リンクもコメントも自由です! お手柔らかに。。。更新のお知らせはTwitter@cut_eliminationで

「直観主義型理論(ITT, Intuitionistic Type Theory)」勉強会ノート其ノ弐拾弐「命題的な(?)等しさ(途中から)」(復習編)

 こちらの復習編。

同一性の除去公理

 わたくし的に気になったのは、プリンキピアでは性質に量化しているがITTではそれができないという点で、集合族を \Pi で束縛することもできるのに何故だろうと思った。しかしITTはどうも高階論理に対応するものではないので、なんかあるのだろう。

左射影規則の逆の証明

 この例はティピカルだと書いてある(34ページ)が、何がティピカルなのかわからなかった。ここの段落の議論は難しくてよくわからない。

性質と要素のインデックス付族

 具体的な導出がわからなかったのでまた次回。