Delooping presented groups in homotopy type theory
This work provides practical improvements for representing groups as loop spaces in homotopy type theory, benefiting researchers in synthetic homotopy theory and formalization of mathematics.
The authors present simplified constructions of deloopings for groups with a known presentation or generating set in homotopy type theory, making them more amenable to computation and metatheoretic reasoning. They also develop a type-theoretic notion of 2-polygraph to manipulate higher inductive types, enabling the construction of Cayley graphs and complexes that encode group relations.
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.