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

Authors Jelle Wemmenhove , Cosmin Manea , Jim Portegies



Document Identifiers

Author Details

Jelle Wemmenhove
  • Department of Mathematics and Computer Science, Eindhoven University of Technology, The Netherlands
Cosmin Manea
  • Department of Mathematics and Computer Science, Eindhoven University of Technology, The Netherlands
Jim Portegies
  • Department of Mathematics and Computer Science, Eindhoven University of Technology, The Netherlands

Content

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

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail