Homotopy Type Theory and the Univalent Approach to Foundations of Mathematics
with Dr Stuart Presnell (Bristol)
In this course we’ll study Homotopy Type Theory (HoTT), with a particular focus on the question of whether it provides a suitable foundation in which to ground mathematics. No prior knowledge of HoTT is assumed, but it would be helpful to have read the first chapter of “Homotopy Type Theory: Univalent Foundations of Mathematics”.
The course will be split across 4 days, as follows:
Day 1: Formalised proof verification — why do we want it, how do we do it, and why might we want Univalence?
Day 2: Identity, Equivalence, and Univalence — what are the consequences of the distinctive way in which Homotopy Type Theory treats identity? What is the role of homotopy in Homotopy Type Theory?
Day 3: Foundational Questions — what does it mean to say that HoTT provides a foundation for mathematics? What are the advantages and disadvantages of taking HoTT as a foundation?
Day 4: Topos Theory — what is the relationship between topos theory and HoTT, and how does this help us to understand the foundational status of HoTT?
