Tsementzis, Dimitris (2017) A Meaning Explanation for HoTT. [Preprint]

Preview

Text A.Meaning.Explanation.for.HoTT.pdf - Submitted Version Download (559kB) | Preview

Abstract

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.

---

Export/Citation:

EndNote | BibTeX | Dublin Core | ASCII/Text Citation (Chicago) | HTML Citation | OpenURL

Social Networking:

Share |

---

Item Type:	Preprint
Creators:	Creators Email ORCID Tsementzis, Dimitris dtsement@princeton.edu
Keywords:	Homotopy Type Theory, Univalent Foundations, Meaning Explanation, Martin-Löf Type Theory
Subjects:	Specific Sciences > Computer Science General Issues > Explanation Specific Sciences > Mathematics
Depositing User:	Dr. Dimitris Tsementzis
Date Deposited:	16 Feb 2017 15:15
Last Modified:	16 Feb 2017 15:15
Item ID:	12824
Subjects:	Specific Sciences > Computer Science General Issues > Explanation Specific Sciences > Mathematics
Date:	15 February 2017
URI:	https://philsci-archive.pitt.edu/id/eprint/12824

Monthly Views for the past 3 years

Monthly Downloads for the past 3 years

Plum Analytics

Actions (login required)

View Item