Homotopy Type Theory and Structuralism

Dissertation, University of Oxford (2014)
Download Edit this record How to cite View on PhilPapers
Abstract
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.
Categories
PhilPapers/Archive ID
THOHTT-7
Upload history
Archival date: 2021-04-03
View other versions
Added to PP index
2021-04-03

Total views
13 ( #58,724 of 58,295 )

Recent downloads (6 months)
13 ( #43,655 of 58,295 )

How can I increase my downloads?

Downloads since first upload
This graph includes both downloads from PhilArchive and clicks on external links on PhilPapers.