# Does Homotopy Type Theory Provide a Foundation for Mathematics?

Ladyman, James and Presnell, Stuart (2014) Does Homotopy Type Theory Provide a Foundation for Mathematics? [Preprint]

 Preview
PDF
Does_HTT_Provide_a_Foundation_public.pdf

## 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 self-contained, 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:
CreatorsEmailORCID
Presnell, Stuart
Keywords: HoTT Homotopy Type Theory foundation mathematics
Subjects: Specific Sciences > Mathematics
Date Deposited: 25 Oct 2014 15:29
Item ID: 11081
Subjects: Specific Sciences > Mathematics
Date: 24 October 2014
URI: http://philsci-archive.pitt.edu/id/eprint/11081