Ladyman, James and Presnell, Stuart (2014) Does Homotopy Type Theory Provide a Foundation for Mathematics? [Preprint]
This is the latest version of this item.

PDF
Does_HTT_Provide_a_Foundation_public.pdf Download (339kB) 
Abstract
Homotopy Type Theory (HoTT) is a putative new foundation for mathematics grounded in constructive intensional type theory, that offers an alternative to the foundations provided by ZFC set theory and category theory. This paper explains and motivates an account of how to define, justify and think about HoTT in a way that is selfcontained, and argues that it can serve as an autonomous foundation for mathematics.
We first consider various questions that a foundation for mathematics might be expected to answer, and find that the standard formulation of HoTT as presented in the ``HoTT Book'' does not answer many of them. More importantly, the way HoTT is developed in the HoTT Book suggests that it is not a candidate \emph{autonomous} foundation since it explicitly depends upon other fields of mathematics, in particular homotopy theory.
We give an alternative presentation of HoTT that does not depend upon sophisticated ideas from other parts of mathematics, and in particular makes no reference to homotopy theory (but is compatible with the homotopy interpretation). Our elaboration of HoTT is based on a new interpretation of types as \emph{mathematical concepts}, which accords with the intensional nature of the type theory.
Export/Citation:  EndNote  BibTeX  Dublin Core  ASCII/Text Citation (Chicago)  HTML Citation  OpenURL 
Social Networking: 
Item Type:  Preprint  

Creators: 


Keywords:  HoTT Homotopy Type Theory foundation mathematics  
Subjects:  Specific Sciences > Mathematics  
Depositing User:  James Ladyman  
Date Deposited:  11 Nov 2014 19:58  
Last Modified:  11 Nov 2014 19:58  
Item ID:  11143  
Subjects:  Specific Sciences > Mathematics  
Date:  24 October 2014  
URI:  https://philsciarchive.pitt.edu/id/eprint/11143 
Available Versions of this Item

Does Homotopy Type Theory Provide a Foundation for Mathematics? (deposited 25 Oct 2014 15:29)
 Does Homotopy Type Theory Provide a Foundation for Mathematics? (deposited 11 Nov 2014 19:58) [Currently Displayed]
Monthly Views for the past 3 years
Monthly Downloads for the past 3 years
Plum Analytics
Actions (login required)
View Item 