Document Open Access Logo

Classifying 2-Groups in Homotopy Type Theory

Authors Perry Hart , Owen Milner

PDF

File

Thumbnail PDF
PDF
LIPIcs.LICS.2026.55.pdf
  • Filesize: 2.53 MB
  • 25 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Theory of computation → Constructive mathematics
  • Theory of computation → Logic and verification
  • Mathematics of computing → Algebraic topology
Keywords
  • homotopy type theory
  • synthetic homotopy theory
  • 2-group
  • higher inductive type
  • bicategory
  • higher group
  • cohomology

Metrics

Abstract

Under the homotopy hypothesis, higher dimensional groups are defined as pointed homotopy types whose homotopy groups vanish outside a certain range. In particular, a 2-group is a pointed connected homotopy 2-type. Classically, 2-groups have two equivalent algebraic descriptions: one in terms of weak monoidal categories and the other in terms of group cohomology. We present these two classifications of pointed connected 2-types in homotopy type theory, thereby providing internal, constructive counterparts to the traditional classifications of 2-groups. Our first classification (in terms of monoidal categories) takes the form of a bicategorical equivalence, while our second is a type equivalence that extends to n-groups for all n ≥ 2. We have mechanized our results in Agda.

Cite As Get BibTex

Perry Hart and Owen Milner. Classifying 2-Groups in Homotopy Type Theory. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 55:1-55:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.LICS.2026.55

Author Details

Perry Hart
  • Department of Computer Science and Engineering, University of Minnesota, Minneapolis, MN, USA
Owen Milner
  • Department of Philosophy, Carnegie Mellon University, Pittsburgh, PA, USA

Funding

This material is based upon work supported by the Air Force Office of Scientific Research under award number FA9550-21-1-0009. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the United States Air Force.

Acknowledgements

We thank Favonia for invaluable comments on the writing of this paper.

Supplementary Materials

References

  1. Benedikt Ahrens, Dan Frumin, Marco Maggesi, Niccolò Veltri, and Niels van der Weide. Bicategories in univalent foundations. Mathematical Structures in Computer Science, 31(10):1232-1269, 2021. URL: https://doi.org/10.1017/S0960129522000032.
  2. Carlo Angiuli, Guillaume Brunerie, Thierry Coquand, Robert Harper, Kuen-Bang Hou (Favonia), and Daniel R. Licata. Syntax and models of Cartesian cubical type theory. Mathematical Structures in Computer Science, 31(4):424-468, 2021. URL: https://doi.org/10.1017/S0960129521000347.
  3. John C. Baez and James Dolan. Categorification. In Ezra Getzler and Mikhail Kapranov, editors, Higher Category Theory, volume 230 of Contemporary Mathematics, pages 1-36, Providence, RI, 1998. American Mathematical Society. URL: https://arxiv.org/abs/9802029.
  4. John C. Baez and Aaron D. Lauda. Higher-dimensional algebra. V: 2-Groups. Theory and Applications of Categories, 12:423-491, 2004. URL: http://eudml.org/doc/124217.
  5. John C. Baez, Danny Stevenson, Alissa S. Crans, and Urs Schreiber. From loop groups to 2-groups. Homology, Homotopy and Applications, 9(2):101-135, 2007. Google Scholar
  6. Tim Baumann. The cup product on cohomology groups in Homotopy Type Theory. Master’s thesis, University of Augsburg, 2018. URL: https://timjb.gitlab.io/masters-thesis/cp-in-hott.pdf.
  7. Ulrik Buchholtz, Floris van Doorn, and Egbert Rijke. Higher Groups in Homotopy Type Theory. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '18, pages 205-214, New York, NY, USA, 2018. Association for Computing Machinery. URL: https://doi.org/10.1145/3209108.3209150.
  8. Ulrik Buchholtz and Johannes Schipp von Branitz. Using displayed univalent graphs to formalize higher groups in univalent foundations. draft version, 2021. URL: https://ulrikbuchholtz.dk/durgs.pdf.
  9. Pierre Cagne, Ulrik Buchholtz, Nicolai Kraus, and Marc Bezem. On symmetries of spheres in univalent foundations, 2024. URL: https://doi.org/10.48550/arXiv.2401.15037.
  10. Josep Elgueta. Permutation 2-groups I: Structure and splitness. Advances in Mathematics, 258:286-350, 2014. URL: https://doi.org/10.1016/j.aim.2014.03.011.
  11. Nick Gurski. Biequivalences in tricategories. Theory and Applications of Categories, 26(14):349-384, 2012. URL: http://www.tac.mta.ca/tac/volumes/26/14/26-14abs.html.
  12. Perry Hart. Mechanized classifications of 2-groups, 2026. Agda code (see the root README for an overview of the codebase). URL: https://github.com/PHart3/2-groups-agda/tree/lics.
  13. Pieter Hofstra and Martti Karvonen. Inner autoequivalences in general and those of monoidal categories in particular. Journal of Pure and Applied Algebra, 228(11):107717, 2024. URL: https://doi.org/10.1016/j.jpaa.2024.107717.
  14. J. R. Isbell and F. B. Wright. Another equivalent form of the axiom of choice. Proceedings of the American Mathematical Society, 17(1):174-174, 1966. URL: https://www.ams.org/journals/proc/1966-017-01/S0002-9939-1966-0186535-8/S0002-9939-1966-0186535-8.pdf.
  15. David Jaz Myers and Zyad Yasser. Higher Schreier Theory in Cubical Agda. The Journal of Symbolic Logic, pages 1-17, 2025. URL: https://doi.org/10.1017/jsl.2024.78.
  16. Niles Johnson and Donald Yau. 2-Dimensional Categories. Oxford University Press, Oxford, January 2021. URL: https://doi.org/10.1093/oso/9780198871378.001.0001.
  17. K. Keremedis. Some equivalents of ac in algebra ii. Algebra Universalis, 39:163-169, August 1998. URL: https://doi.org/10.1007/s000120050073.
  18. 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), CSL-LICS '14, New York, NY, USA, 2014. Association for Computing Machinery. URL: https://doi.org/10.1145/2603088.2603153.
  19. 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.
  20. Saunders MacLane and J. H. C. Whitehead. On the 3-Type of a Complex. Proceedings of the National Academy of Sciences, 36(1):41-48, 1950. URL: https://doi.org/10.1073/pnas.36.1.41.
  21. J. P. May. A Concise Course in Algebraic Topology. Chicago Lectures in Mathematics. University of Chicago Press, Chicago, 1999. URL: https://www.math.uchicago.edu/~may/CONCISE/ConciseRevised.pdf.
  22. 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. URL: https://doi.org/10.1145/3661814.3662077.
  23. Anders Mörtberg and Loïc Pujet. Cubical synthetic homotopy theory. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, pages 158-171, New York, NY, USA, 2020. Association for Computing Machinery. URL: https://doi.org/10.1145/3372885.3373825.
  24. nLab authors. bigroupoid. https://ncatlab.org/nlab/show/bigroupoid, May 2025. URL: https://ncatlab.org/nlab/revision/bigroupoid/5.
  25. Behrang Noohi. Notes on 2-Groupoids, 2-Groups and Crossed Modules. Homology, Homotopy and Applications, 9(1):75-106, 2007. Google Scholar
  26. Egbert Rijke. Introduction to Homotopy Type Theory, 2022. URL: https://arxiv.org/abs/2212.11082.
  27. Egbert Rijke, Michael Shulman, and Bas Spitters. Modalities in homotopy type theory. Logical Methods in Computer Science, Volume 16, Issue 1, January 2020. URL: https://doi.org/10.23638/LMCS-16(1:2)2020.
  28. Michael Shulman. All (∞,1)-toposes have strict univalent universes, 2019. URL: https://arxiv.org/abs/1904.07004.
  29. Mike Shulman. Fibrations with fiber an Eilenberg-MacLane space. https://homotopytypetheory.org/2014/06/30/fibrations-with-em-fiber/, June 2014. Homotopy Type Theory blog, accessed 2026-04-21.
  30. Jonathan Sterling and Carlo Angiuli. Normalization for Cubical Type Theory. In 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-15, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470719.
  31. Andrew W Swan. On the Nielsen-Schreier Theorem in Homotopy Type Theory. Logical Methods in Computer Science, Volume 18, Issue 1, January 2022. URL: https://doi.org/10.46298/lmcs-18(1:18)2022.
  32. Andrew W Swan. Computable and non-computable 2-groups in HoTT. In Workshop on Homotopy Type Theory / Univalent Foundations 2025, 2025. URL: https://hott-uf.github.io/2025/abstracts/HoTTUF_2025_paper_13.pdf.
  33. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
  34. Niccolò Veltri and Niels van der Weide. Constructing Higher Inductive Types as Groupoid Quotients. Logical Methods in Computer Science, Volume 17, Issue 2, April 2021. URL: https://doi.org/10.23638/LMCS-17(2:8)2021.
  35. 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:e8, 2021. URL: https://doi.org/10.1017/S0956796821000034.
  36. David Wärn. Eilenberg–Maclane spaces and stabilisation in homotopy type theory. Journal of Homotopy and Related Structures, 18(2):357-368, September 2023. URL: https://doi.org/10.1007/s40062-023-00330-5.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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