DROPS

Artifact

Software

Formalization of Classification of Covering Spaces and Canonical Change of Basepoint in HoTT

Authors: Jelle Wemmenhove, Cosmin Manea, and Jim Portegies

Abstract

Cite as

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)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-22492,
   title = {{Formalization of Classification of Covering Spaces and Canonical Change of Basepoint in HoTT}}, 
   author = {Wemmenhove, Jelle and Manea, Cosmin and Portegies, Jim},
   note = {Software, version 0.3., swhId: \href{https://archive.softwareheritage.org/swh:1:dir:bea0c0af55e3ec9869679f3a5611cc5154a9ddbf;origin=https://gitlab.tue.nl/computer-verified-proofs/covering-spaces;visit=swh:1:snp:6b1d9a68d2f10e958534db29214f30ddd1dd9db3;anchor=swh:1:rev:cfc827a2b07f8cb93b412bd6e551d31fae044fb9}{\texttt{swh:1:dir:bea0c0af55e3ec9869679f3a5611cc5154a9ddbf}} (visited on 2024-11-28)},
   url = {https://gitlab.tue.nl/computer-verified-proofs/covering-spaces},
   doi = {10.4230/artifacts.22492},
}

Document

DOI: 10.4230/LIPIcs.TYPES.2023.1

Classification of Covering Spaces and Canonical Change of Basepoint

Authors: Jelle Wemmenhove, Cosmin Manea, and Jim Portegies

Published in: LIPIcs, Volume 303, 29th International Conference on Types for Proofs and Programs (TYPES 2023)

Abstract

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

Cite as

Jelle Wemmenhove, Cosmin Manea, and Jim Portegies. Classification of Covering Spaces and Canonical Change of Basepoint. In 29th International Conference on Types for Proofs and Programs (TYPES 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 303, pp. 1:1-1:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{wemmenhove_et_al:LIPIcs.TYPES.2023.1,
  author =	{Wemmenhove, Jelle and Manea, Cosmin and Portegies, Jim},
  title =	{{Classification of Covering Spaces and Canonical Change of Basepoint}},
  booktitle =	{29th International Conference on Types for Proofs and Programs (TYPES 2023)},
  pages =	{1:1--1:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-332-4},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{303},
  editor =	{Kesner, Delia and Reyes, Eduardo Hermo and van den Berg, Benno},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2023.1},
  URN =		{urn:nbn:de:0030-drops-204795},
  doi =		{10.4230/LIPIcs.TYPES.2023.1},
  annote =	{Keywords: Synthetic Homotopy Theory, Homotopy Type Theory, Covering Spaces, Change-of-Basepoint Isomorphism}
}

Search Results

Documents authored by Wemmenhove, Jelle

Formalization of Classification of Covering Spaces and Canonical Change of Basepoint in HoTT

Abstract

Cite as

Classification of Covering Spaces and Canonical Change of Basepoint

Abstract

Cite as

Thanks for your feedback!

Could not send message