The Integers in Homotopy Type Theory
University of Nottingham
Abstract: Homotopy Type Theory (HoTT) is a foundational approach to Mathematics
based on Martin-Löf’s Type Theory and Voevodsky’s univalence principle. It
addresses the fundamental mismatch between equivalence and equality by identifying the two. However, there is a price to pay if we want our definitions to
interact well with higher order structures.
I will give a general overview over HoTT focussing on motivations and then
discuss the definition of the integers or more general of free groups over a set
as an example of how to address coherence issues that emerge in HoTT. I will
also discuss other related questions such as HoTT in HoTT.
The talk is based on joint work with Luis Scoccola.