Dissertation, University of Oxford (2014)

Teruji Thomas
Oxford University
I explore the possibility of a structuralist interpretation of homotopy type theory (HoTT) as a foundation for mathematics. There are two main aspects to HoTT's structuralist credentials. First, it builds on categorical set theory (CST), of which the best-known variant is Lawvere's ETCS. I argue that CST has merit as a structuralist foundation, in that it ascribes only structural properties to typical mathematical objects. However, I also argue that this success depends on the adoption of a strict typing system which undermines the metaphysical seriousness of this structuralism. Homotopy type theory adds to CST a distinctive theory of identity between sets, which arguably allows its objects to be seen as ante rem structures. I examine the prospects for such a view, and address many other interpretive problems as they arise.
Keywords Mathematical structuralism  Homotopy type theory  Category theory  Dependent type theory  Categorical set theory
Categories (categorize this paper)
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy

 PhilArchive page | Other versions
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

No references found.

Add more references

Citations of this work BETA

No citations found.

Add more citations

Similar books and articles

Does Homotopy Type Theory Provide a Foundation for Mathematics?James Ladyman & Stuart Presnell - 2016 - British Journal for the Philosophy of Science:axw006.
What Types Should Not Be.Bruno Bentzen - 2020 - Philosophia Mathematica 28 (1):60-76.
Structuralism, Invariance, and Univalence.Steve Awodey - 2014 - Philosophia Mathematica 22 (1):1-11.
Univalent polymorphism.Benno van den Berg - 2020 - Annals of Pure and Applied Logic 171 (6):102793.
Universes and Univalence in Homotopy Type Theory.James Ladyman & Stuart Presnell - 2019 - Review of Symbolic Logic 12 (3):426-455.
Constructive Mathematics and Equality.Bruno Bentzen - 2018 - Dissertation, Sun Yat-Sen University


Added to PP index

Total views
17 ( #598,064 of 2,426,897 )

Recent downloads (6 months)
17 ( #43,908 of 2,426,897 )

How can I increase my downloads?


My notes