Artifact
Formalization of Classification of Covering Spaces and Canonical Change of Basepoint in HoTT Software
Authors
Jelle Wemmenhove 
,
Cosmin Manea ,
Jim Portegies
- Part of: Collection: Supplementary Materials
- License: BSD 2-Clause "Simplified" License
- Publication Date: 2024-11-28
Document Identifiers
Author Details
- Department of Mathematics and Computer Science, Eindhoven University of Technology, The Netherlands
- Department of Mathematics and Computer Science, Eindhoven University of Technology, The Netherlands
Content
- Software (Source Code): https://gitlab.tue.nl/computer-verified-proofs/covering-spaces
-
archived version
Version/Status
- Content created at: 2024-05-30
- Status: Inactive (at the time of publication 2024-11-28)
Cite As Get BibTex
Jelle Wemmenhove, Cosmin Manea, Jim Portegies. Formalization of Classification of Covering Spaces and Canonical Change of Basepoint in HoTT (Software, Source Code). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/artifacts.22492
Description
Formal proof in Homotopy Type Theory (HoTT) of classification of covering spaces and the existence of canonical change-of-basepoint isomorphisms between homotopy groups. The latter is shown to be related and in some cases equivalent to trivial actions of the fundamental group on (higher) homotopy groups.
Subject Classification
Keywords
- Synthetic Homotopy Theory
- Homotopy Type Theory
- Covering Spaces
- Change-of-Basepoint Isomorphism
Programming Languages
- Gallina (Coq)
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)