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