2025/12/10 by Samuel Mimram, Mimram, Samuel, Émile Oleon +1
Mathematics · #Advanced Topology and Set Theory #Algebraic Topology (math.AT) #FOS: Computer and information sciences #FOS: Mathematics #Geometric and Algebraic Topology #Homotopy and Cohomology in Algebraic Topology #Logic in Computer Science (cs.LO)
paper · doi:10.48550/arxiv.2512.10064
openalex publication_date 2025/12/10 · openalex created_date 2025/12/13 · openalex updated_date 2026/07/28
Covering spaces are a fundamental tool in algebraic topology because of the close relationship they bear with the fundamental groups of spaces. Indeed, they are in correspondence with the subgroups of the fundamental group: this is known as the Galois correspondence. In particular, the covering space corresponding to the trivial group is the universal covering, which is a "1-connected" variant of the original space, in the sense that it has the same homotopy groups, except for the first one which is trivial. In this article, we formalize this correspondence in homotopy type theory, a variant of Martin-Löf type theory in which types can be interpreted as spaces (up to homotopy). Along the way, we develop an n-dimensional generalization of covering spaces. Moreover, in order to demonstrate the applicability of our approach, we formally classify the covering of lens spaces and explain how to construct the Poincaré homology sphere.