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
...
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.
