Does Homotopy Type Theory Provide a Foundation for Mathematics?

British Journal for the Philosophy of Science:axw006 (2016)
  Copy   BIBTEX


Homotopy Type Theory 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 article explains and motivates an account of how to define, justify, and think about HoTT in a way that 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, 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. 1 Introduction2 What Is a Foundation for Mathematics?2.1 A characterization of a foundation for mathematics2.2 Autonomy3 The Basic Features of Homotopy Type Theory3.1 The rules3.2 The basic ways to construct types3.3 Types as propositions and propositions as types3.4 Identity3.5 The homotopy interpretation4 Autonomy of the Standard Presentation?5 The Interpretation of Tokens and Types5.1 Tokens as mathematical objects?5.2 Tokens and types as concepts6 Justifying the Elimination Rule for Identity7 The Foundations of Homotopy Type Theory without Homotopy7.1 Framework7.2 Semantics7.3 Metaphysics7.4 Epistemology7.5 Methodology8 Possible Objections to this Account8.1 A constructive foundation for mathematics?8.2 What are concepts?8.3 Isn’t this just Brouwerian intuitionism?8.4 Duplicated objects8.5 Intensionality and substitution salva veritate9 Conclusion9.1 Advantages of this foundation.



    Upload a copy of this work     Papers currently archived: 77,697

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Set-Theoretic Foundations.Stewart Shapiro - 2000 - The Proceedings of the Twentieth World Congress of Philosophy 2000:183-196.
Category theory as an autonomous foundation.Øystein Linnebo & Richard Pettigrew - 2011 - Philosophia Mathematica 19 (3):227-254.
Metaphysics and the Foundations of Mathematics.Vasilii Ya Perminov - 2012 - Russian Studies in Philosophy 50 (4):24-42.


Added to PP

200 (#66,623)

6 months
6 (#144,124)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Stuart Presnell
University of Bristol

References found in this work

The Indispensability of Mathematics.Mark Colyvan - 2001 - Oxford, England: Oxford University Press.
An Unsolvable Problem of Elementary Number Theory.Alonzo Church - 1936 - Journal of Symbolic Logic 1 (2):73-74.
Mathematics without foundations.Hilary Putnam - 1967 - Journal of Philosophy 64 (1):5-22.
Science without numbers, A Defence of Nominalism.Hartry Field - 1980 - Revue Philosophique de la France Et de l'Etranger 171 (4):502-503.

View all 30 references / Add more references