Calculating the Fundamental Group of the Circle in Homotopy Type Theory
Formalized in the Coq Unimath library
J.T. van Heiningen (TU Delft - Electrical Engineering, Mathematics and Computer Science)
Benedikt Ahrens – Mentor (TU Delft - Programming Languages)
Kobe Wullaert – Graduation committee member (TU Delft - Programming Languages)
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 goal of this paper is to formalize the Fundamental Group of the Circle within Coq and the Unimath library, as described in the paper by Mr Licata and Mr Shulman, and show it is isomorphic to Z. Fundamental groups are a powerful algebraic invariant for studying Homotopy theory, and provide deep, yet concise insights into the fundamental properties of a space.