[HoTT]HoTTをこっそり学ぶ その3 Martin-Lfのextensional版とintensional版についてもう少し追及してみる。その後の調査では、というようなidentity typeの導入（intensional identity typeと呼ばれるそうな）があるものをintensional版と理解すればよいよう…

[HoTT]HoTTをこっそり学ぶ その2 さて、まずはMartin-Lf依存型理論というのを勉強せんといかんわけだが、調べれば調べるほどなんだかとっ散らかっている感がある。標準的な定式化というのがあるようなないような、バリエーションも多く、表記の違いなのか何…