Calculating the Fundamental Group of the Circle in Homotopy Type Theory: Formalized in the Coq Unimath library
2023
Online
Elektronische Ressource
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.
CSE3000 Research Project
Computer Science and Engineering
Titel: |
Calculating the Fundamental Group of the Circle in Homotopy Type Theory: Formalized in the Coq Unimath library
|
---|---|
Link: | |
Veröffentlichung: | 2023 |
Medientyp: | Elektronische Ressource |
Schlagwort: |
|
Sonstiges: |
|