A Meaning Explanation for HoTT

Publication Year:
Usage 760
Downloads 760
Repository URL:
Tsementzis, Dimitris
preprint description
The Univalent Foundations (UF) offer a new picture of the foundations of mathematics largely independent from set theory. In this paper I will focus on the question of whether Homotopy Type Theory (HoTT) (as a formalization of UF) can be justified intuitively as a theory of shapes in the same way that ZFC (as a formalization of set-theoretic foundations) can be justified intuitively as a theory of collections. I first clarify what I mean by an “intuitive justification” by distinguishing between formal and pre- formal “meaning explanations” in the vein of Martin-Löf. I then explain why Martin-Löf’s original meaning explanation for type theory no longer applies to HoTT. Finally, I outline a pre-formal meaning explanation for HoTT based on spatial notions like “shape”, “path”, “point” etc. which in particular provides an intuitive justification of the axiom of univalence. I conclude by discussing the limitations and prospects of such a project.