%0 Journal Article %1 noauthororeditor %A Ladyman, James %A Presnell, Stuart %D 2018 %J The British Journal for the Philosophy of Science %K 03a05-philosophical-and-critical-aspects-of-mathematical-logic-and-foundations 03b15-higher-order-logic-type-theory %N 2 %P 377-420 %R https://doi.org/10.1093/bjps/axw006 %T Does homotopy type theory provide a foundation for mathematics? %U https://academic.oup.com/bjps/article-abstract/69/2/377/2669763?redirectedFrom=fulltext %V 69 %X 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 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 (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.

@article{noauthororeditor, 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 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 (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. }, added-at = {2019-05-20T01:20:06.000+0200}, author = {Ladyman, James and Presnell, Stuart}, biburl = {https://www.bibsonomy.org/bibtex/23edafbc13bb5099095a3c287dc28fa7b/gdmcbain}, description = {Zbl 1400.03012}, doi = {https://doi.org/10.1093/bjps/axw006}, interhash = {0954f4e2623d01ab2083f00fc2b7582c}, intrahash = {3edafbc13bb5099095a3c287dc28fa7b}, journal = {The British Journal for the Philosophy of Science}, keywords = {03a05-philosophical-and-critical-aspects-of-mathematical-logic-and-foundations 03b15-higher-order-logic-type-theory}, number = 2, pages = {377-420}, timestamp = {2019-05-20T01:20:06.000+0200}, title = {Does homotopy type theory provide a foundation for mathematics?}, url = {https://academic.oup.com/bjps/article-abstract/69/2/377/2669763?redirectedFrom=fulltext}, volume = {69 }, year = 2018 }