The Proof of the Fundamental Group of the Circle in Homotopy Type Theory’s Dependence on the Univalence Axiom
A.C. Linssen (TU Delft - Electrical Engineering, Mathematics and Computer Science)
Benedikt Ahrens – Mentor (TU Delft - Programming Languages)
K.F. Wullaert – Mentor (TU Delft - Programming Languages)
R. Hai – Graduation committee member (TU Delft - Web Information Systems)
More Info
expand_more
Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.
Abstract
The incorporation of the univalence axiom into homotopy type theory has facilitated a new way of proving a basic result in algebraic topology: that the fundamental group of the circle is the integers (π1(S1) ≃ Z). This proof is formalised by Licata and Shulman. However, while the authors note that the univalence axiom is essential, it is not clearly stated where and why. A step-by-step analysis of their proof, the purpose of which is to increase the readers’ understanding of the univalence axiom and its implications in homotopy type theory, shows that it relies on the univalence axiom for constructing the circle. When assuming axiom K instead of the univalence axiom, we can no longer construct the circle in the same way, leading to π1(S1) ≃ 1.