PhilSci Archive

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]

This is the latest version of this item.

[img]
Preview
 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 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:
Share |
Item Type: Preprint
Creators:
CreatorsEmailORCID
Ladyman, James
Presnell, Stuart
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://philsci-archive.pitt.edu/id/eprint/11143

Available Versions of this Item

Monthly Views for the past 3 years

Monthly Downloads for the past 3 years

Plum Analytics

Actions (login required)

View Item View Item