Classification of Covering Spaces and Canonical Change of Basepoint

TL;DR

This paper uses homotopy type theory to synthetically prove a classification theorem for covering spaces and investigates canonical basepoint change isomorphisms, with mechanized proofs in Coq.

Contribution

It introduces a synthetic proof of the covering space classification theorem within HoTT and explores canonical basepoint isomorphisms, simplifying classical concepts.

Findings

Synthetic proof of the classification theorem for covering spaces

Existence of canonical change-of-basepoint isomorphisms in homotopy groups

Mechanized proofs using Coq closely follow classical topology treatments

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.