Calculating the Fundamental Group of the Circle in Homotopy Type Theory
Formalized in the Coq Unimath library
Bachelor Thesis
(2023)
Faculty
Electrical Engineering, Mathematics and Computer Science
To reference this document use:
https://resolver.tudelft.nl/uuid:4b14b07d-4ffd-42c3-9b31-51293e6f8820
More Info
expand_more
expand_more
Publication Year
2023
Language
English
Graduation Date
25-06-2023
Awarding Institution
Delft University of Technology
Faculty
Electrical Engineering, Mathematics and Computer Science
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.
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.