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

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 settheoretic 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 MartinLöf. I then explain why MartinLöf’s original meaning explanation for type theory no longer applies to HoTT. Finally, I outline a preformal 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: 
Item Type:  Preprint  

Creators: 


Keywords:  Homotopy Type Theory, Univalent Foundations, Meaning Explanation, MartinLö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:  http://philsciarchive.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 