PhilSci Archive

A Meaning Explanation for HoTT

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

[img]
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:
CreatorsEmailORCID
Tsementzis, Dimitrisdtsement@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-dev.library.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 View Item