Delooping presented groups in homotopy type theory

TL;DR

This paper explores methods for constructing group deloopings in homotopy type theory, simplifying the process when a group's presentation is known, and develops tools for manipulating higher inductive types.

Contribution

It introduces simplified constructions for group deloopings using known presentations and develops a type-theoretic notion of 2-polygraph for higher inductive types.

Findings

Simpler variants of delooping constructions are more computationally friendly.

Developed a type-theoretic 2-polygraph for manipulating higher inductive types.

Formalized developments in the cubical Agda proof assistant.

Abstract

Homotopy type theory is a logical setting based on Martin-L\"of 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.