Document Open Access Logo

Cellular Methods in Homotopy Type Theory

Authors Axel Ljungström , Loïc Pujet

PDF

File

Thumbnail PDF
PDF
LIPIcs.LICS.2026.66.pdf
  • Filesize: 1.93 MB
  • 25 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
Keywords
  • Homotopy type theory
  • Univalent foundations
  • constructive mathematics
  • synthetic homotopy theory
  • CW complexes
  • cellular homology
  • Hurewicz theorem

Metrics

Abstract

In classical mathematics, a CW complex is a topological space which can be built up inductively by gluing together cells of increasing dimension. Thanks to their excellent categorical properties, CW complexes have become one of the main objects of interest in algebraic topology. Although their quasi-combinatorial nature suggests that a constructive treatment is possible, there seems to be little literature on the subject - perhaps because of the important role played by the axiom of choice in the classical theory of CW complexes.
In this paper, we present a synthetic and constructive account of the theory of CW complexes in homotopy type theory. Our first main result is a finitary version of the cellular approximation theorem which, among other things, allows us to construct a cellular homology functor without needing the axiom of choice or relying on a pre-existing notion of homology. Our second main result, which we call the "Hurewicz approximation theorem", shows that the CW complexes that are n-connected types are precisely the ones that can be presented by a CW structure with no nontrivial cells up to dimension n. This theorem is standard in the classical treatment of CW complexes, but it is far from being obvious in a constructive setting. As a corollary, we give a new proof of the Hurewicz theorem for CW complexes, which relates the first non-vanishing homotopy group of a CW complex with the corresponding homology group. All key theorems presented in this paper have been mechanised in Cubical Agda.

Cite As Get BibTex

Axel Ljungström and Loïc Pujet. Cellular Methods in Homotopy Type Theory. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 66:1-66:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.LICS.2026.66

Author Details

Axel Ljungström
  • School of Computer Science, University of Nottingham, UK
Loïc Pujet
  • ICube, University of Strasbourg, France

Funding

  • Ljungström, Axel: Knut & Alice Wallenberg Foundation’s Program for Mathematics.

Acknowledgements

We would like to thank Anders Mörtberg whose ideas on computational aspects of cellular (co)homology were one of the original motivations behind this project. We also wish to thank him - as well as Reid Barton and Owen Milner - for many fruitful discussions about the application of our work to the proof and formalisation of the Serre finiteness theorem. Finally, we express gratitude to the anonymous reviewers of this paper for their thorough readings and useful suggestions for improvements.

Supplementary Materials

References

  1. Reid Barton and Tim Campion. A synthetic approach to finite presentability of homotopy groups. Preprint, 2026. URL: https://github.com/CMU-HoTT/serre-finiteness/blob/main/Paper/barton-campion.pdf.
  2. Guillaume Brunerie. On the homotopy groups of spheres in homotopy type theory. PhD thesis, Université Nice Sophia Antipolis, 2016. URL: https://arxiv.org/abs/1606.05916.
  3. Guillaume Brunerie, Axel Ljungström, and Anders Mörtberg. Synthetic Integral Cohomology in Cubical Agda. In Florin Manea and Alex Simpson, editors, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022), volume 216 of Leibniz International Proceedings in Informatics (LIPIcs), pages 11:1-11:19, Dagstuhl, Germany, 2022. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CSL.2022.11.
  4. Ulrik Buchholtz and Kuen-Bang Hou Favonia. Cellular Cohomology in Homotopy Type Theory. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '18, pages 521-529, New York, NY, USA, 2018. Association for Computing Machinery. URL: https://doi.org/10.1145/3209108.3209188.
  5. Pierre Cagne, Ulrik Torben Buchholtz, Nicolai Kraus, and Marc Bezem. On symmetries of spheres in univalent foundations. 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.3662115.
  6. Evan Cavallo. Synthetic Cohomology in Homotopy Type Theory. Master’s thesis, Carnegie Mellon University, 2015. Google Scholar
  7. J Daniel Christensen and Luis Scoccola. The Hurewicz theorem in homotopy type theory. Algebraic & Geometric Topology, 23(5):2107-2140, July 2023. URL: https://doi.org/10.2140/agt.2023.23.2107.
  8. Robert Graham. Synthetic Homology in Homotopy Type Theory, 2018. Preprint. URL: https://arxiv.org/abs/1706.01540.
  9. Kuen-Bang Hou (Favonia), Eric Finster, Daniel R. Licata, and Peter LeFanu Lumsdaine. A Mechanization of the Blakers-Massey Connectivity Theorem in Homotopy Type Theory. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, pages 565-574, New York, NY, USA, 2016. ACM. URL: https://doi.org/10.1145/2933575.2934545.
  10. Thomas Lamiaux, Axel Ljungström, and Anders Mörtberg. Computing cohomology rings in cubical agda. In Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023, pages 239-252, New York, NY, USA, 2023. Association for Computing Machinery. URL: https://doi.org/10.1145/3573105.3575677.
  11. Daniel R. Licata and Michael Shulman. Calculating the Fundamental Group of the Circle in Homotopy Type Theory. In Proceedings of the 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '13, pages 223-232, Washington, DC, USA, 2013. IEEE Computer Society. URL: https://doi.org/10.1109/LICS.2013.28.
  12. Axel Ljungström and Loïc Pujet. Cellular Methods in Homotopy Type Theory (accompanying formalisation). Software, Knut and Alice Wallenberg Foundation Postdoctoral Scholarship: Program in Mathematics for researchers with a Swedish doctor’s degree, swhId: https://archive.softwareheritage.org/swh:1:dir:7904cf81046d351ce2a27f778d8b96f71186035d;origin=https://github.com/agda/cubical;visit=swh:1:snp:82843e2d41d4b8b6a9013ffeadeb01fbcbb23e53;anchor=swh:1:rev:8a45d739ad0b75f4773874be4a5e42dbd46c9cd6 (visited on 2026-06-29). URL: https://github.com/agda/cubical/blob/master/Cubical/Papers/CellularMethods.agda, URL: https://doi.org/10.4230/artifacts.26875.
  13. Axel Ljungström and Anders Mörtberg. Formalizing π₄(S³)≅ℤ/2ℤ and Computing a Brunerie Number in Cubical Agda . In 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-13, Los Alamitos, CA, USA, June 2023. IEEE Computer Society. URL: https://doi.org/10.1109/LICS56636.2023.10175833.
  14. 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.
  15. J.P. May. A Concise Course in Algebraic Topology. Chicago Lectures in Mathematics. University of Chicago Press, 1999. Google Scholar
  16. Owen Milner. Formalizing the Whitehead tower in cubical agda, 2023. Talk at the Seminar on Homotopy Type Theory at CMU. URL: https://lc2023.unimi.it/wp-content/uploads/2023/05/milner.pdf.
  17. Egbert Rijke. Introduction to Homotopy Type Theory, 2022. URL: https://arxiv.org/abs/2212.11082.
  18. Michael Shulman. All (∞,1)-toposes have strict univalent universes, April 2019. Preprint. URL: https://arxiv.org/abs/1904.07004.
  19. Kristina Sojakova, Floris van Doorn, and Egbert Rijke. Sequential Colimits in Homotopy Type Theory. In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '20, pages 845-858, New York, NY, USA, 2020. Association for Computing Machinery. URL: https://doi.org/10.1145/3373718.3394801.
  20. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. Self-published, Institute for Advanced Study, 2013. URL: https://homotopytypetheory.org/book/.
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