PhilSci Archive

Identity in HoTT, Part I

Ladyman, James and Presnell, Stuart (2014) Identity in HoTT, Part I. [Preprint]

This is the latest version of this item.


Download (331kB)


Homotopy type theory (HoTT) is a new branch of mathematics that connects algebraic topology with logic and computer science, and which has been proposed as a new language and conceptual framework for math- ematical practice. Much of the power of HoTT lies in the correspondence between the formal type theory and ideas from homotopy theory, in par- ticular the interpretation of types, tokens, and equalities as (respectively) spaces, points, and paths. Fundamental to the use of identity and equality in HoTT is the powerful proof technique of path induction. In the ‘HoTT Book’ this principle is justified through the homotopy interpretation of type theory, by treating identifications as paths and the induction step as a homotopy between paths. This is incompatible with HoTT being an au- tonomous foundation for mathematics, since any such foundation must be able to justify its principles without recourse to existing areas of mathemat- ics. In this paper it is shown that path induction can be motivated from pre-mathematical considerations, and in particular without recourse to ho- motopy theory. This makes HoTT a candidate for being an autonomous foundation for mathematics.

Export/Citation: EndNote | BibTeX | Dublin Core | ASCII/Text Citation (Chicago) | HTML Citation | OpenURL
Social Networking:
Share |

Item Type: Preprint
Ladyman, James
Presnell, Stuart
Keywords: HoTT foundation mathematics identity path induction
Subjects: Specific Sciences > Mathematics
Depositing User: James Ladyman
Date Deposited: 11 Nov 2014 20:03
Last Modified: 11 Nov 2014 20:03
Item ID: 11142
Subjects: Specific Sciences > Mathematics
Date: 23 October 2014

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