[HoTT]HoTTをこっそり学ぶ その10 さて、すでに終盤に突入している。2.4.1節に取り組もう。ホモトピー解釈からさらに進んで、Martin-Lf型理論をホモトピー理論の論理学としたいのである。 2.4. Higher algebraic structures ホモトピー解釈によって本質的に…