2026-07-25T12:50:06Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:20479 2024-11-27T23:17:54Z ddc:004 open_access

Classification of Covering Spaces and Canonical Change of Basepoint Wemmenhove, Jelle Manea, Cosmin Portegies, Jim Synthetic Homotopy Theory Homotopy Type Theory Covering Spaces Change-of-Basepoint Isomorphism Using the language of homotopy type theory (HoTT), we 1) prove a synthetic version of the classification theorem for covering spaces, and 2) explore the existence of canonical change-of-basepoint isomorphisms between homotopy groups. There is some freedom in choosing how to translate concepts from classical algebraic topology into HoTT. The final translations we ended up with are easier to work with than the ones we started with. We discuss some earlier attempts to shed light on this translation process. The proofs are mechanized using the Coq proof assistant and closely follow classical treatments like those by Hatcher [Allen Hatcher, 2002]. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Jelle Wemmenhove and Cosmin Manea and Jim Portegies 2024 Is Part Of LIPIcs, Volume 303, 29th International Conference on Types for Proofs and Programs (TYPES 2023) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TYPES.2023.1 urn:nbn:de:0030-drops-204795 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2023.1 eng https://creativecommons.org/licenses/by/4.0/legalcode