💻 computer science

Delooping presented groups in homotopy type theory

This paper presents simplified, computationally efficient methods for constructing deloopings of presented groups in homotopy type theory using generating sets, and introduces a type-theoretic 2-polygraph framework to analyze the resulting higher inductive types and their associated Cayley graphs and complexes, with developments formalized in Cubical Agda.

Original authors: Camil Champin, Samuel Mimram, Emile Oleon

Published 2026-05-01

📖 4 min read☕ Coffee break read

CC BY 4.0

Original authors: Camil Champin, Samuel Mimram, Emile Oleon

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Imagine you are trying to describe a complex dance routine (a Group) to a robot that only understands geometry and movement (Homotopy Type Theory). In this world, mathematical "types" are like shapes or spaces, and proving things is like drawing paths between points on those shapes.

The paper you're asking about is about finding the best, simplest way to build a "stage" (a mathematical space) where this dance routine can happen. This stage is called a delooping.

Here is the breakdown of their work, using simple analogies:

1. The Problem: Two Ways to Build the Stage

The authors explain that there are two standard ways to build this stage for any group, but both can be a bit clunky or "heavy" if you have a lot of dancers.

Method A (The Torsor): Imagine you have a huge library of every possible way the group could interact with a set of objects. You pick one specific "master interaction" (the principal torsor) and look only at the neighborhood around it. It works, but it's like trying to find a specific book by looking at the entire library first.
Method B (The Higher Inductive Type): Imagine building the stage from scratch using Lego bricks. You put down a central point, then you add a loop (a string tied in a circle) for every single move the group can make, and then you add rules (glue) to make sure the loops combine correctly. If your group has 100 moves, you need 100 loops and hundreds of glue rules. This is very heavy and hard to compute.

2. The Solution: Using the "Cheat Sheet" (Generators)

The authors' main discovery is that if you know the generators of the group (the basic moves from which all other moves are built), you can build a much smaller, lighter stage.

The Analogy: Instead of adding a loop for every single move in a 100-move dance, you only add loops for the 3 basic moves (the generators) that can be combined to make the other 97.
The Result:
- For Method A: Instead of tracking how the group acts on everything, you only track how the generators act. It's like describing a dance by only listing the steps for the lead dancer, knowing the rest follow automatically.
- For Method B: Instead of building 100 loops, you build 3. You add glue rules only for the basic combinations that define the group's structure. This makes the "stage" much easier for computers to handle and for mathematicians to reason about.

3. The Tool: 2-Polygraphs (The Blueprint)

To manage these new, smaller stages, the authors introduce a tool called a 2-polygraph.

The Analogy: Think of a 2-polygraph as a blueprint or a flowchart for the stage.
- Points are the locations on the stage.
- Lines are the basic moves (generators).
- Shapes (like squares or bubbles) are the rules that tell you how to combine moves (relations).
Why it helps: This blueprint allows them to use standard group theory tricks (like Tietze transformations) to rewrite the blueprint into a simpler version without changing the actual dance. It's like editing a recipe to use fewer ingredients while keeping the taste exactly the same.

4. The Visuals: Cayley Graphs and Complexes

The paper also looks at how to visualize the "difference" between a free group (a group with no rules, just pure movement) and a real group (which has rules).

The Cayley Graph: Imagine a map where every dot is a position in the dance, and every arrow is a step you can take. This map shows you all the possible paths.
The Cayley Complex: This is the graph with "walls" or "floors" added in. If you have a rule that says "Step A then Step B is the same as Step C," the complex adds a flat surface connecting those paths. It measures the "holes" or "loops" in the dance that are forced by the rules.
The Insight: The authors show that these maps and surfaces are exactly what you get when you mathematically "subtract" the rules from the free movement. They provide a way to see the group's structure visually.

Summary

In short, the paper says: "If you know the basic ingredients (generators) of a group, you don't need to build a massive, complicated mathematical machine to represent it. You can build a tiny, efficient version using fewer loops and rules, and we have a new set of blueprints (polygraphs) to help us design and simplify these versions."

This makes it easier for computers (specifically the Agda proof assistant) to verify mathematical proofs about these groups because the "machines" they are checking are much smaller and simpler.

1. Problem Statement

In Homotopy Type Theory (HoTT), groups can be represented in two ways:

External (Concrete): As sets equipped with multiplication, unit, and inverse operations satisfying axioms.
Internal (Abstract): As the loop space $\Omega A$ of a pointed connected groupoid $A$ . The type $A$ is called the delooping of the group, denoted $BG$.

While the existence of deloopings is well-established (e.g., via the torsor construction or Eilenberg-MacLane spaces), constructing them for presented groups (groups defined by generators and relations) using standard methods often results in types that are computationally heavy and difficult to reason about.

The standard torsor construction requires considering the action of the entire group, leading to large types.
The standard Higher Inductive Type (HIT) construction (Finster-Licata) defines $BG$ with loops for every group element and identities for every multiplication entry, which is redundant for presented groups and complicates inductive proofs.

The authors aim to develop simpler, more efficient constructions for deloopings when a presentation (generators and relations) is known, making them amenable to computation and metatheoretic reasoning (e.g., cohomology calculations).

2. Methodology

The paper utilizes the synthetic approach of HoTT, leveraging:

Higher Inductive Types (HITs): To define spaces with points, paths (loops), and higher paths (identities between paths).
Truncation: Using propositional ( $\|-1$ ) and set ( $\|0$ ) truncations to manage homotopy levels.
Polygraphs: Adapting the concept of 2-polygraphs (from rewriting theory and $\omega$ -categories) to HoTT to manipulate HITs internally.
Fiber Sequences and Grothendieck Duality: To relate group actions, torsors, and kernels.

The authors formalize these concepts in Cubical Agda, ensuring constructive validity.

3. Key Contributions

A. Simplified Torsor Constructions for Generated Groups

The authors refine the classical torsor construction (based on $G$ -sets) for groups with a known generating set $X$ .

Standard Approach: The delooping is the connected component of the principal $G$ -torsor in the type of all $G$ -sets ( $Set_G$ ). This requires preserving the action of all elements of $G$ .
New Approach: They define $X$ -sets (sets equipped with an action only of the generators $X$ ). They prove that the connected component of the principal $X$ -torsor in the type of $X$ -sets ( $Set_X$ ) is also a delooping of $G$ .
Result: This yields a significantly smaller type. For example, for the cyclic group $\mathbb{Z}$ , the delooping is the connected component of the successor function in the type of endomorphisms, rather than the full type of $\mathbb{Z}$ -sets. This avoids the need for Higher Inductive Types in specific contexts (like UniMath) and simplifies reasoning.

B. Efficient HIT Constructions for Presented Groups

For groups defined by a presentation $\langle X \mid R \rangle$ , the authors propose a "smaller" HIT for the delooping $BG$.

Standard HIT: Loops for every $g \in G$ and relations for every multiplication $g \cdot h$ .
Proposed HIT ($BP$):
- One point $\star$ .
- One loop gen for each generator $x \in X$ .
- One 2-cell (identity) rel for each relation $r \in R$ .
- A groupoid truncation constructor.
Significance: This matches the combinatorial structure of the group presentation. It reduces the number of constructors, making inductive proofs (e.g., for homology or cohomology) much more tractable. It allows for proofs based on Tietze transformations.

C. 2-Polygraphs in HoTT

To formally reason about these HITs, the authors introduce 2-polygraphs within HoTT.

Definition: A structure consisting of 0-cells (points), 1-cells (generators), and 2-cells (relations), indexed by spheres.
Correspondence: They show that the type generated by a 2-polygraph $P$ corresponds exactly to the HIT $BP$ constructed above.
Tietze Transformations: They define Tietze transformations (adding/removing generators and relations) for 2-polygraphs and prove that these transformations preserve the presented type (Theorem 29). This allows for the internal manipulation of group presentations (e.g., converting to a convergent presentation) without changing the underlying homotopy type.

D. Cayley Graphs and Complexes

The authors provide a synthetic construction of Cayley graphs and complexes as kernels of maps between deloopings.

Cayley Graph ( $C(X, G)$ ): Defined as the kernel of the map $B\gamma^*: BX^* \to BG$ (where $X^*$ is the free group). They prove this type is precisely the Cayley graph of $G$ with respect to $X$ .
Cayley Complex: Defined as the kernel of the map from the 2-skeleton of the delooping ( $B_2P$ ) to the full delooping ($BG$).
Significance: This establishes Cayley graphs as the "difference" between the free group delooping and the actual group delooping. The Cayley complex measures relations between relations. They prove these structures are universal coverings (or higher coverings) of the respective types.

4. Key Results

Theorem 15: The connected component of the principal $X$ -torsor is a delooping of $G$ if $X$ generates $G$ .
Theorem 24: The HIT generated by generators $X$ and relations $R$ (with groupoid truncation) is a delooping of the presented group $[P]$ .
Theorem 29: Tietze transformations on 2-polygraphs preserve the presented type (i.e., $\|P\|_1 = \|Q\|_1$ ).
Theorem 35: The Cayley graph $C(X, G)$ is the kernel of the map $BX^* \to BG$ .
Theorem 40: The Cayley complex $CP$ fits into a fiber sequence $CP \to B_2P \to BG$ , acting as the universal 1-covering of $B_2P$ .

5. Significance

Computational Efficiency: The proposed constructions are "smaller" than standard ones, reducing the complexity of type-checking and inductive reasoning in proof assistants like Agda.
Bridging Algebra and Topology: The work successfully internalizes classical group-theoretic concepts (presentations, Cayley graphs, Tietze transformations) into the synthetic language of HoTT.
Metatheoretic Reasoning: By using 2-polygraphs, the authors enable the use of rewriting techniques (like Knuth-Bendix completion) to compute invariants (homology, cohomology) of groups directly within the type theory.
Formalization: A significant portion of the theory is formalized in Cubical Agda, providing a verified foundation for future work on group cohomology and higher group actions.
Future Directions: The paper lays the groundwork for defining $n$ -polygraphs and higher Cayley complexes, potentially leading to automated computation of higher homotopy groups and coherence data for groups.

In summary, this paper provides a toolkit for constructing and manipulating group deloopings that are tailored to the specific presentation of the group, making them more practical for synthetic mathematics and computer verification.