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
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)
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.
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)