Document Open Access Logo

Delooping Generated Groups in Homotopy Type Theory

Authors Camil Champin, Samuel Mimram , Émile Oleon

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2024.6.pdf
  • Filesize: 0.75 MB
  • 20 pages

Document Identifiers

Author Details

Camil Champin
  • École Normale Supérieure de Lyon, France
Samuel Mimram
  • LIX, CNRS, École polytechnique, Institut Polytechnique de Paris, Palaiseau, France
Émile Oleon
  • LIX, CNRS, École polytechnique, Institut Polytechnique de Paris, Palaiseau, France

Acknowledgements

We would like to thank Dan Christensen as well as an anonymous reviewer for useful comments on early drafts of this article.

Cite AsGet BibTex

Camil Champin, Samuel Mimram, and Émile Oleon. Delooping Generated Groups in Homotopy Type Theory. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 6:1-6:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.FSCD.2024.6

Abstract

Homotopy type theory is a logical setting based on Martin-Löf type theory in which one can perform geometric constructions and proofs in a synthetic way. Namely, types can be interpreted as spaces (up to continuous deformation) and proofs as homotopy invariant constructions. In this context, loop spaces of pointed connected groupoids provide a natural representation of groups, and any group can be obtained as the loop space of such a type, which is then called a delooping of the group. There are two main methods to construct the delooping of an arbitrary group G. The first one consists in describing it as a pointed higher inductive type, whereas the second one consists in taking the connected component of the principal G-torsor in the type of sets equipped with an action of G. We show here that, when a presentation is known for the group, simpler variants of those constructions can be used to build deloopings. The resulting types are more amenable to computations and lead to simpler meta-theoretic reasoning. We also investigate, in this context, an abstract construction for the Cayley graph of a generated group and show that it encodes the relations of the group. Most of the developments performed in the article have been formalized using the cubical version of the Agda proof assistant.

Subject Classification

ACM Subject Classification
  • Theory of computation → Constructive mathematics
Keywords
  • homotopy type theory
  • delooping
  • group
  • generator
  • Cayley graph

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Dimitri Ara, Albert Burroni, Yves Guiraud, Philippe Malbos, François Métayer, and Samuel Mimram. Polygraphs: From rewriting to higher categories. To appear, 2023. URL: https://arxiv.org/abs/2312.00429.
  2. Marc Bezem, Ulrik Buchholtz, Pierre Cagne, Bjørn Ian Dundas, and Daniel R. Grayson. Symmetry. URL: https://github.com/UniMath/SymmetryBook.
  3. 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. URL: https://doi.org/10.1016/j.jpaa.2021.106687.
  4. Guillaume Brunerie, Axel Ljungström, and Anders Mörtberg. Synthetic integral cohomology in cubical Agda. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.CSL.2022.11.
  5. Ulrik Buchholtz, J Daniel Christensen, Jarl G Taxerås Flaten, and Egbert Rijke. Central H-spaces and banded types. Preprint, 2023. URL: https://arxiv.org/abs/2301.02636.
  6. Ulrik Buchholtz and Kuen-Bang Hou. Cellular cohomology in homotopy type theory. Logical Methods in Computer Science, 16, 2020. URL: https://doi.org/10.23638/LMCS-16(2:7)2020.
  7. Ulrik Buchholtz and Egbert Rijke. The real projective spaces in homotopy type theory. In 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-8. IEEE, 2017. URL: https://doi.org/10.5555/3329995.3330081.
  8. Evan Cavallo. Synthetic cohomology in homotopy type theory. PhD thesis, MA thesis, 2015. Google Scholar
  9. Arthur Cayley. Desiderata and suggestions. No. 2 - The theory of groups: graphical representation. American journal of mathematics, 1(2):174-176, 1878. Google Scholar
  10. Camil Champin and Samuel Mimram. Delooping generated groups in homotopy type theory. Software, swhId: https://archive.softwareheritage.org/swh:1:dir:4fc863802e40f99733703893622a7aa23c50c308;origin=https://github.com/smimram/generated-deloopings-agda;visit=swh:1:snp:209bea02bef97c56fbcc2da7af07f6b27e89b12c;anchor=swh:1:rev:6b457f58ef54a2ef8e7338fbe7d56a893cc79831 (visited on 2024-06-20). URL: https://github.com/smimram/generated-deloopings-agda.
  11. Thierry Coquand and Nils Anders Danielsson. Isomorphism is equality. Indagationes Mathematicae, 24(4):1105-1120, 2013. URL: https://doi.org/10.1016/j.indag.2013.09.002.
  12. Michel Demazure and Pierre Gabriel. Groupes Algébriques, Tome 1. North-Holland Publishing Company, 1970. Google Scholar
  13. John RJ Groves. Rewriting systems and homology of groups. In Groups—Canberra 1989: Australian National University Group Theory Program 1989, pages 114-141. Springer, 2006. URL: https://doi.org/10.1007/BFb0100735.
  14. 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. URL: https://doi.org/10.4171/jems/1050.
  15. Nicolai Kraus and Thorsten Altenkirch. Free higher groups in homotopy type theory. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, pages 599-608, 2018. URL: https://doi.org/10.1145/3209108.3209183.
  16. Nicolai Kraus and Jakob von Raumer. A rewriting coherence theorem with applications in homotopy type theory. Mathematical Structures in Computer Science, 32(7):982-1014, 2022. URL: https://doi.org/10.1017/S0960129523000026.
  17. Daniel R Licata and Eric Finster. Eilenberg-MacLane spaces in homotopy type theory. In Proceedings 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. URL: https://doi.org/10.1145/2603088.2603153.
  18. Peter LeFanu Lumsdaine and Michael Shulman. Semantics of higher inductive types. Mathematical Proceedings of the Cambridge Philosophical Society, 169(1):159-208, 2020. URL: https://doi.org/10.1017/S030500411900015X.
  19. Roger C Lyndon and Paul E Schupp. Combinatorial group theory, volume 188. Springer, 1977. Google Scholar
  20. Per Martin-Löf. Intuitionistic type theory, volume 1 of Studies in proof theory. Bibliopolis, 1984. Google Scholar
  21. Émile Oleon and Samuel Mimram. Delooping cyclic groups with lens spaces in homotopy type theory. Accepted at LICS 2024 conference, 2024. Google Scholar
  22. Henri Poincaré. Analysis situs. Gauthier-Villars Paris, France, 1895. Google Scholar
  23. Egbert Rijke. The join construction. Preprint, 2017. URL: https://arxiv.org/abs/1701.07538.
  24. Egbert Rijke. Classifying Types. PhD thesis, Carnegie Mellon University, July 2018. URL: https://arxiv.org/abs/1906.09435.
  25. Egbert Rijke. Introduction to homotopy type theory. Preprint, 2022. URL: https://arxiv.org/abs/2212.11082.
  26. The Agda Community. Cubical Agda Library, July 2023. URL: https://github.com/agda/cubical.
  27. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study, 2013. URL: https://homotopytypetheory.org/book/.
  28. 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. URL: https://doi.org/10.1145/3341691.
  29. David Wärn. Eilenberg-maclane spaces and stabilisation in homotopy type theory. Journal of Homotopy and Related Structures, 18(2):357-368, 2023. URL: https://doi.org/10.1007/s40062-023-00330-5.
  30. David Wärn. Path spaces of pushouts. Preprint, 2023. URL: https://arxiv.org/abs/2402.12339.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact