Samuel Mimram

Camil Champin, Samuel Mimram, Emile Oleon

Homotopy type theory is a logical setting based on Martin-Löf type theory in which geometric constructions and proofs can be carried out synthetically. Here, types can be interpreted as spaces up to homotopy, and proofs as homotopy-invariant constructions. In this context, the loop spaces of pointed connected groupoids provide a natural representation of groups, and every group can be realized as the loop space of such a type, which is then called a delooping of the group. There are two main methods for constructing a delooping of an arbitrary group G. The first describes it as a pointed higher inductive type, while the second takes the connected component of the principal G-torsor in the type of sets equipped with a G-action. We show that, when a presentation, or even just a generating set, is known for the group, simpler variants of these constructions can be used to build deloopings. The resulting types are more amenable to computation and lead to simpler metatheoretic reasoning. Finally, we develop a type-theoretic notion of 2-polygraph for manipulating higher inductive types such as those arising in the description of deloopings. This allows us to investigate a construction of the Cayley graph of a generated group and to show that it encodes the relations of the group, as well as a Cayley complex encoding relations between relations. Many of the developments in this article have been formalized in the cubical version of the Agda proof assistant.

Samuel Mimram, Émile Oleon

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.