Homotopy Type Theory and Structuralism

Dissertation, University of Oxford (2014)
  Copy   BIBTEX


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.

Author's Profile

Teruji Thomas
Oxford University


Added to PP

236 (#60,609)

6 months
79 (#47,907)

Historical graph of downloads since first upload
This graph includes both downloads from PhilArchive and clicks on external links on PhilPapers.
How can I increase my downloads?