The Proof of the Fundamental Group of the Circle in Homotopy Type Theory’s Dependence on the Univalence Axiom

Bachelor thesis (2022)

Authors

A.C. Linssen Electrical Engineering, Mathematics and Computer Science

Contributors

B.P. Ahrens Programming Languages - EEMCS (mentor)
K.F. Wullaert Programming Languages - EEMCS (mentor)
R. Hai Web Information Systems - EEMCS (graduation committee member)
Faculty
Electrical Engineering, Mathematics and Computer Science, Electrical Engineering, Mathematics and Computer Science
Copyright: © 2022 Anneke Linssen
More Info
expand_more

Published Date

22-06-2022

Language

English

Reuse Rights

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.

Faculty

Electrical Engineering, Mathematics and Computer Science

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.

Files

CSE3000_paper.pdf
(.pdf | 0.596 Mb)