Does Homotopy Type Theory Provide a Foundation for Mathematics?

James Ladyman, Stuart Presnell

Research output: Contribution to journalArticle (Academic Journal)

4 Citations (Scopus)

Abstract

Homotopy Type Theory (HoTT) is a putative newfoundation for mathematics grounded in constructive intensional type theory that offers an alternative to the foundations provided by ZFC set theory and category theory. This article explains and motivates an account of how to define, justify, and think about HoTT in awaythat is self-contained, and argues that, so construed, it is a candidate for being an autonomous foundation for mathematics. We first consider various questions that a foundation for mathematics might be expected to answer, and find that many of them are not answered by the standard formulation of HoTT as presented in the 'HoTT Book'. More importantly, the presentation of HoTT given in the HoTT Book is not autonomous 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 ideas from other parts of mathematics, and in particular makes no reference to homotopy theory (but is compatible with the homotopy interpretation), and argue that it is a candidate autonomous foundation for mathematics. Our elaboration of HoTT is based on a new interpretation of types as mathematical concepts, which accords with the intensional nature of the type theory.

Original languageEnglish
Pages (from-to)377-420
Number of pages44
JournalBritish Journal for the Philosophy of Science
Volume69
Issue number2
DOIs
Publication statusPublished - 22 Sep 2016

Structured keywords

  • Centre for Science and Philosophy
  • Centre_for_science_and_philosophy

Fingerprint Dive into the research topics of 'Does Homotopy Type Theory Provide a Foundation for Mathematics?'. Together they form a unique fingerprint.

Cite this