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