Calculating the Fundamental Group of the Circle in Homotopy Type Theory

Formalized in the Coq Unimath library

Bachelor thesis (2023)

Authors

J.T. van Heiningen Electrical Engineering, Mathematics and Computer Science

Contributors

Benedikt Ahrens Programming Languages (mentor)
K.F. Wullaert Programming Languages (graduation committee member)
Faculty
Electrical Engineering, Mathematics and Computer Science, Electrical Engineering, Mathematics and Computer Science
Copyright: © 2023 Jeroen van Heiningen
More Info
expand_more

Published Date

25-06-2023

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

Files

Final_Academic_Paper_2_1.pdf
(pdf | 1.71 Mb)
Unknown license