pith. sign in

arxiv: 2405.03264 · v3 · submitted 2024-05-06 · 💻 cs.LO · math.CT

Delooping presented groups in homotopy type theory

Camil Champin , Samuel Mimram , Emile Oleon This is my paper

Pith reviewed 2026-05-24 01:45 UTC · model grok-4.3

classification 💻 cs.LO math.CT
keywords homotopy type theorydeloopinghigher inductive typesgroup presentationpolygraphCayley graphtorsorcubical Agda
0
0 comments X

The pith

For groups with a known presentation, simpler delooping constructions work in homotopy type theory.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper shows that when a group is given by a presentation or generating set, the two standard delooping constructions in homotopy type theory can be simplified. One construction uses a pointed higher inductive type and the other extracts the connected component of a principal G-torsor. These reduced versions produce types that support direct computation and require less metatheoretic machinery. The authors introduce a type-theoretic 2-polygraph to manage the relations encoded in such higher inductive types and apply it to construct the Cayley graph and Cayley complex of the group. All developments are formalized in cubical Agda.

Core claim

When a presentation or even just a generating set is known for the group G, simpler variants of the two main delooping constructions can be used: a pointed higher inductive type and the connected component of the principal G-torsor in the type of sets equipped with a G-action. The resulting types are more amenable to computation and lead to simpler metatheoretic reasoning. A type-theoretic notion of 2-polygraph is developed for manipulating higher inductive types, which allows construction of the Cayley graph encoding the relations of the group and the Cayley complex encoding relations between relations.

What carries the argument

Simpler variants of the pointed higher inductive type and principal G-torsor delooping constructions, together with the type-theoretic 2-polygraph for encoding and manipulating relations in higher inductive types.

If this is right

  • The deloopings become directly amenable to computation.
  • Metatheoretic arguments about the deloopings become simpler.
  • The Cayley graph of a generated group encodes its relations.
  • The Cayley complex encodes relations between relations.
  • The constructions can be carried out and verified inside cubical Agda.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • These reduced constructions may support direct calculation of group invariants inside proof assistants.
  • The 2-polygraph notion could extend to higher-dimensional presentations of homotopy types.
  • The link between presentations and deloopings clarifies how rewriting systems interact with synthetic group theory.

Load-bearing premise

The group must be presented or generated by a known set.

What would settle it

A specific group equipped with an explicit generating set or presentation for which the simplified higher inductive type or torsor component fails to have the original group as its loop space.

Figures

Figures reproduced from arXiv: 2405.03264 by Camil Champin, Emile Oleon, Samuel Mimram.

Figure 1
Figure 1. Figure 1: Cayley complex of the quaternion group. Proof. Writing ⋆ for the point corresponding to the neutral element of the group, we have to show that the type ∥⋆ = x∥0 is contractible, for any vertex x : G. Since the Cayley complex is connected as a quotient of a connected space (Proposition 36) and being contractible is a proposition, we can suppose that we have a path ⋆ = x and therefore, by path induction, we … view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 2 minor

Summary. The paper claims that when a presentation or generating set is known for a group G, simpler variants of the two standard delooping constructions (a pointed higher inductive type and the connected component of the principal G-torsor) can be used in homotopy type theory. These yield types more amenable to computation and simpler metatheoretic reasoning. The work further develops a type-theoretic notion of 2-polygraph, uses it to construct the Cayley graph (whose 1-skeleton encodes generators) and Cayley complex (encoding relations between relations), and states that many of these developments have been formalized in cubical Agda.

Significance. If the constructions hold, the explicit use of known generators to reduce the number of constructors in the delooping HITs and torsor constructions provides a practical advance for computational synthetic homotopy theory of groups. The machine-checked formalization in cubical Agda is a clear strength, directly supporting the encoding properties of the polygraph, Cayley graph, and complex rather than leaving them as unverified claims.

major comments (1)
  1. [§3] The central claim that the simpler variants remain deloopings (i.e., that their loop spaces recover G) is load-bearing; the manuscript presents them as direct type-theoretic definitions, but a explicit comparison to the standard HIT/torsor definitions (showing preservation of the group structure) would be needed in the section introducing the variants.
minor comments (2)
  1. [§4] Notation for the 2-polygraph constructors and the precise statement of how 2-cells encode relations could be clarified with a small diagram or table relating the polygraph data to the Cayley graph 1-skeleton.
  2. The abstract states that 'many of the developments' are formalized; an explicit list of which theorems or constructions are covered by the Agda code would help readers assess the scope of the machine-checked support.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the positive assessment and for highlighting the importance of our formalization. We address the single major comment below.

read point-by-point responses

  1. Referee: [§3] The central claim that the simpler variants remain deloopings (i.e., that their loop spaces recover G) is load-bearing; the manuscript presents them as direct type-theoretic definitions, but a explicit comparison to the standard HIT/torsor definitions (showing preservation of the group structure) would be needed in the section introducing the variants.

    Authors: We agree that an explicit comparison to the standard delooping constructions would strengthen the presentation and make the load-bearing claim more transparent. While the manuscript already proves directly that the loop spaces of the simpler variants recover G, we will revise §3 to include a dedicated comparison: we will define canonical maps from our presented-group variants to the standard HIT and torsor deloopings and prove that these maps induce equivalences on loop spaces (hence preserve the group structure). This addition will be self-contained and will not alter the subsequent developments on 2-polygraphs or the formalization. revision: yes

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper defines delooping constructions directly as higher inductive types and torsor-based types in homotopy type theory, with simpler variants explicitly conditioned on a known presentation or generating set. These are then used to define a 2-polygraph whose properties (Cayley graph encoding relations, Cayley complex) are shown by direct construction. The central claims rest on these explicit definitions rather than any reduction to fitted parameters, self-referential equations, or load-bearing self-citations. The manuscript notes that the developments have been formalized in cubical Agda, providing independent machine-checked verification outside the paper's own text. No step equates a derived quantity to its input by construction or imports uniqueness via prior author work.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The work rests on standard homotopy type theory axioms for higher inductive types and pointed connected groupoids; no free parameters or invented entities are introduced beyond the new constructions themselves.

axioms (1)
  • standard math Standard HoTT rules for higher inductive types and loop spaces of pointed connected groupoids
    Invoked to interpret groups as loop spaces and to define deloopings as HITs.

pith-pipeline@v0.9.0 · 5792 in / 1164 out tokens · 20991 ms · 2026-05-24T01:45:27.476425+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. Classifying covering types in homotopy type theory

    cs.LO 2025-12 unverdicted novelty 7.0

    Formalizes the Galois correspondence for covering spaces in homotopy type theory with n-dimensional generalization and demonstrates it on lens spaces and the Poincaré sphere.

Reference graph

Works this paper leans on

42 extracted references · 42 canonical work pages · cited by 1 Pith paper · 3 internal anchors

  1. [1]

    Cubical Agda library

    The Agda Community. Cubical Agda library. URL:https://github.com/agda/cubical

    work page

  2. [2]

    Polygraphs: From Rewriting to Higher Categories

    Dimitri Ara, Albert Burroni, Yves Guiraud, Philippe Malbos, François Métayer, and Samuel Mimram. Polygraphs: From Rewriting to Higher Categories. London Mathematical Society Lecture Note Series. Cambridge University Press, 2025.doi:10.1017/9781009498968

    work page doi:10.1017/9781009498968 2025

  3. [3]

    Marc Bezem, Ulrik Buchholtz, Pierre Cagne, Bjørn Ian Dundas, and Daniel R. Grayson. Symmetry. URL:https://github.com/UniMath/SymmetryBook

    work page

  4. [4]

    Construction of the circle in UniMath.Journal of Pure and Applied Algebra, 225(10):106687, 2021.doi:10.1016/j.jpaa.2021

    Marc Bezem, Ulrik Buchholtz, Daniel R Grayson, and Michael Shulman. Construction of the circle in UniMath.Journal of Pure and Applied Algebra, 225(10):106687, 2021.doi:10.1016/j.jpaa.2021. 106687

    work page doi:10.1016/j.jpaa.2021 2021

  5. [5]

    On the homotopy groups of spheres in homotopy type theory

    Guillaume Brunerie.On the homotopy groups of spheres in homotopy type theory. PhD thesis, Université de Nice, 2016.arXiv:1606.05916

    work page internal anchor Pith review Pith/arXiv arXiv 2016

  6. [6]

    Synthetic integral cohomology in cubical Agda

    Guillaume Brunerie, Axel Ljungström, and Anders Mörtberg. Synthetic integral cohomology in cubical Agda. In30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Schloss Dagstuhl- Leibniz-Zentrum für Informatik, 2022.doi:10.4230/LIPIcs.CSL.2022.11

    work page doi:10.4230/lipics.csl.2022.11 2022

  7. [7]

    Daniel Christensen, Jarl G

    Ulrik Buchholtz, J. Daniel Christensen, Jarl G. Taxerås Flaten, and Egbert Rijke. Central H-spaces and banded types.Journal of Pure and Applied Algebra, 229(6):107963, 2025.doi:10.1016/j.jpaa.2025. 107963

    work page doi:10.1016/j.jpaa.2025 2025

  8. [8]

    Cellular cohomology in homotopy type theory.Logical Methods in Computer Science, 16, 2020.doi:10.23638/LMCS-16(2:7)2020

    Ulrik Buchholtz and Kuen-Bang Hou. Cellular cohomology in homotopy type theory.Logical Methods in Computer Science, 16, 2020.doi:10.23638/LMCS-16(2:7)2020

    work page doi:10.23638/lmcs-16(2:7)2020 2020

  9. [9]

    The real projective spaces in homotopy type theory

    Ulrik Buchholtz and Egbert Rijke. The real projective spaces in homotopy type theory. In2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1–8. IEEE, 2017. doi:10.5555/3329995.3330081

    work page doi:10.5555/3329995.3330081 2017

  10. [10]

    Higher-dimensional word problems with applications to equational logic.Theoretical computer science, 115(1):43–62, 1993.doi:10.1016/0304-3975(93)90054-W

    Albert Burroni. Higher-dimensional word problems with applications to equational logic.Theoretical computer science, 115(1):43–62, 1993.doi:10.1016/0304-3975(93)90054-W

    work page doi:10.1016/0304-3975(93)90054-w 1993

  11. [11]

    Synthetic cohomology in homotopy type theory, 2015

    Evan Cavallo. Synthetic cohomology in homotopy type theory, 2015. Master’s thesis, Carnegie Mellon University

    work page 2015

  12. [12]

    Desiderata and suggestions

    Arthur Cayley. Desiderata and suggestions. No. 2 – The theory of groups: graphical representation. American journal of mathematics, 1(2):174–176, 1878

    work page

  13. [13]

    Delooping generated groups

    Camil Champin and Samuel Mimram. Delooping generated groups. URL:https://github.com/smimram/ generated-deloopings-agda

    work page

  14. [14]

    Delooping generated groups in homotopy type theory

    Camil Champin, Samuel Mimram, and Émile Oleon. Delooping generated groups in homotopy type theory. In Jakob Rehof, editor,9th International Conference on Formal Structures for Computation 38 DELOOPING PRESENTED GROUPS IN HOMOTOPY TYPE THEORY and Deduction (FSCD 2024), volume 299 ofLIPIcs, page 6:1–6:20. Schloss Dagstuhl, 2024. doi: 10.4230/LIPIcs.FSCD.2024.6

    work page doi:10.4230/lipics.fscd.2024.6 2024

  15. [15]

    Isomorphism is equality.Indagationes Mathematicae, 24(4):1105–1120, 2013.doi:10.1016/j.indag.2013.09.002

    Thierry Coquand and Nils Anders Danielsson. Isomorphism is equality.Indagationes Mathematicae, 24(4):1105–1120, 2013.doi:10.1016/j.indag.2013.09.002

    work page doi:10.1016/j.indag.2013.09.002 2013

  16. [16]

    North-Holland Publishing Company, 1970

    Michel Demazure and Pierre Gabriel.Groupes Algébriques, Tome 1. North-Holland Publishing Company, 1970

    work page 1970

  17. [17]

    John R. J. Groves. Rewriting systems and homology of groups. InGroups—Canberra 1989: Australian Na- tional University Group Theory Program 1989, pages 114–141. Springer, 2006.doi:10.1007/BFb0100735

    work page doi:10.1007/bfb0100735 1989

  18. [18]

    Covering spaces in homotopy type theory

    Robert Harper and Kuen-Bang Hou (Favonia). Covering spaces in homotopy type theory. In22nd International Conference on Types for Proofs and Programs (TYPES 2016), pages 11–1. Schloss Dagstuhl– Leibniz-Zentrum für Informatik, 2018.doi:10.4230/LIPIcs.TYPES.2016.11

    work page doi:10.4230/lipics.types.2016.11 2016

  19. [19]

    The simplicial model of Univalent Foundations (after Voevodsky).Journal of the European Mathematical Society, 23(6):2071–2126, 2021.doi:10.4171/jems/ 1050

    Krzysztof Kapulkin and Peter LeFanu Lumsdaine. The simplicial model of Univalent Foundations (after Voevodsky).Journal of the European Mathematical Society, 23(6):2071–2126, 2021.doi:10.4171/jems/ 1050

    work page doi:10.4171/jems/ 2071

  20. [20]

    A finite Thue system with decidable word problem and without equivalent finite canonical system.Theoretical Computer Science, 35:337–344, 1985.doi:10.1016/ 0304-3975(85)90023-4

    Deepak Kapur and Paliath Narendran. A finite Thue system with decidable word problem and without equivalent finite canonical system.Theoretical Computer Science, 35:337–344, 1985.doi:10.1016/ 0304-3975(85)90023-4

    work page 1985

  21. [21]

    Knuth and Peter B

    Donald E. Knuth and Peter B. Bendix. Simple word problems in universal algebras.Automation of Reasoning: 2: Classical Papers on Computational Logic 1967–1970, pages 342–376, 1983.doi: 10.1016/B978-0-08-012975-4.50028-X

    work page doi:10.1016/b978-0-08-012975-4.50028-x 1967

  22. [22]

    Free higher groups in homotopy type theory

    Nicolai Kraus and Thorsten Altenkirch. Free higher groups in homotopy type theory. InProceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, pages 599–608, 2018. doi:10.1145/3209108.3209183

    work page doi:10.1145/3209108.3209183 2018

  23. [23]

    A rewriting coherence theorem with applications in ho- motopy type theory.Mathematical Structures in Computer Science, 32(7):982–1014, 2022

    Nicolai Kraus and Jakob von Raumer. A rewriting coherence theorem with applications in ho- motopy type theory.Mathematical Structures in Computer Science, 32(7):982–1014, 2022. doi: 10.1017/S0960129523000026

    work page doi:10.1017/s0960129523000026 2022

  24. [24]

    Aesop: White-Box Best-First Proof Search for Lean

    Thomas Lamiaux, Axel Ljungström, and Anders Mörtberg. Computing cohomology rings in cubical Agda. InProceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, pages 239–252, 2023.doi:10.1145/3573105.3575677

    work page doi:10.1145/3573105.3575677 2023

  25. [25]

    Eilenberg-MacLane spaces in homotopy type theory

    Daniel R Licata and Eric Finster. Eilenberg-MacLane spaces in homotopy type theory. InProceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1–9, 2014.doi:10.1145/2603088.2603153

    work page doi:10.1145/2603088.2603153 2014

  26. [26]

    Computational synthetic cohomology theory in homotopy type theory.Mathematical Structures in Computer Science, 35, 2025.doi:10.1017/S0960129525000131

    Axel Ljungström and Anders Mörtberg. Computational synthetic cohomology theory in homotopy type theory.Mathematical Structures in Computer Science, 35, 2025.doi:10.1017/S0960129525000131

    work page doi:10.1017/s0960129525000131 2025

  27. [27]

    Semantics of higher inductive types.Mathematical Pro- ceedings of the Cambridge Philosophical Society, 169(1):159–208, 2020.doi:10.1017/S030500411900015X

    Peter LeFanu Lumsdaine and Michael Shulman. Semantics of higher inductive types.Mathematical Pro- ceedings of the Cambridge Philosophical Society, 169(1):159–208, 2020.doi:10.1017/S030500411900015X

    work page doi:10.1017/s030500411900015x 2020

  28. [28]

    Lyndon and Paul E

    Roger C. Lyndon and Paul E. Schupp.Combinatorial group theory, volume 188. Springer, 1977

    work page 1977

  29. [29]

    Bibliopolis, 1984

    Per Martin-Löf.Intuitionistic type theory, volume 1 ofStudies in proof theory. Bibliopolis, 1984

    work page 1984

  30. [30]

    Delooping cyclic groups with lens spaces in homotopy type theory

    Samuel Mimram and Emile Oleon. Delooping cyclic groups with lens spaces in homotopy type theory. In Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’24, New York, NY, USA, 2024. Association for Computing Machinery.doi:10.1145/3661814.3662077

    work page doi:10.1145/3661814.3662077 2024

  31. [31]

    Coherent Tietze transformations of 1-polygraphs in homotopy type theory

    Samuel Mimram and Émile Oleon. Coherent Tietze transformations of 1-polygraphs in homotopy type theory. In10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025), volume 337 ofLeibniz International Proceedings in Informatics (LIPIcs), page 30:1–30:17. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2025.doi:10.4230/...

    work page doi:10.4230/lipics.fscd.2025.30 2025

  32. [32]

    Hypercubical manifolds in homotopy type theory

    Samuel Mimram and Émile Oleon. Hypercubical manifolds in homotopy type theory. Submitted, 2025. arXiv:2506.19402

    work page arXiv 2025

  33. [33]

    Classifying covering types in homotopy type theory

    Samuel Mimram and Émile Oleon. Classifying covering types in homotopy type theory. In34th EACSL Annual Conference on Computer Science Logic (CSL 2026), volume 363 ofLeibniz International Proceedings in Informatics (LIPIcs), page 21:1–21:20. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2026.doi:10.4230/LIPIcs.CSL.2026.21

    work page doi:10.4230/lipics.csl.2026.21 2026

  34. [34]

    Gauthier-Villars Paris, France, 1895

    Henri Poincaré.Analysis situs. Gauthier-Villars Paris, France, 1895

    work page

  35. [35]

    The join construction

    Egbert Rijke. The join construction. Unpublished manuscript, 2017.arXiv:1701.07538

    work page internal anchor Pith review Pith/arXiv arXiv 2017

  36. [36]

    Classifying Types

    Egbert Rijke.Classifying Types. PhD thesis, Carnegie Mellon University, July 2018.arXiv:1906.09435. DELOOPING PRESENTED GROUPS IN HOMOTOPY TYPE THEORY 39

    work page internal anchor Pith review Pith/arXiv arXiv 2018

  37. [37]

    Cambridge Studies in Advanced Mathematics

    Egbert Rijke.Introduction to Homotopy Type Theory. Cambridge Studies in Advanced Mathematics. Cambridge University Press, 2025

    work page 2025

  38. [38]

    Über die topologischen Invarianten mehrdimensionaler Mannigfaltigkeiten.Monatshefte für Mathematik und Physik, 19:1–118, 1908

    Heinrich Tietze. Über die topologischen Invarianten mehrdimensionaler Mannigfaltigkeiten.Monatshefte für Mathematik und Physik, 19:1–118, 1908

    work page 1908

  39. [39]

    Institute for Advanced Study, 2013

    The Univalent Foundations Program.Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study, 2013. URL:https://homotopytypetheory.org/book/

    work page 2013

  40. [40]

    Cubical A gda: a Dependently Typed Programming Language With Univalence and Higher Inductive Types

    Andrea Vezzosi, Anders Mörtberg, and Andreas Abel. Cubical Agda: A dependently typed programming language with univalence and higher inductive types.Journal of Functional Programming, 31, 2021. doi:10.1145/3341691

    work page doi:10.1145/3341691 2021

  41. [41]

    Eilenberg–Maclane spaces and stabilisation in homotopy type theory.Journal of Homotopy and Related Structures, 18(2):357–368, 2023.doi:10.1007/s40062-023-00330-5

    David Wärn. Eilenberg–Maclane spaces and stabilisation in homotopy type theory.Journal of Homotopy and Related Structures, 18(2):357–368, 2023.doi:10.1007/s40062-023-00330-5

    work page doi:10.1007/s40062-023-00330-5 2023

  42. [42]

    Path spaces of pushouts

    David Wärn. Path spaces of pushouts. Preprint, 2023.arXiv:2402.12339

    work page arXiv 2023