Document Open Access Logo

Synthetic Integral Cohomology in Cubical Agda

Authors Guillaume Brunerie, Axel Ljungström, Anders Mörtberg

PDF
Thumbnail PDF

File

LIPIcs.CSL.2022.11.pdf
  • Filesize: 0.85 MB
  • 19 pages

Document Identifiers

Author Details

Guillaume Brunerie
  • Independent researcher, Stockholm, Sweden
Axel Ljungström
  • Department of Mathematics, Stockholm University, Sweden
Anders Mörtberg
  • Department of Mathematics, Stockholm University, Sweden

Funding

The material in this paper is based upon research supported by the Swedish Research Council (SRC, Vetenskapsrådet) under Grant No. 2019-04545.

Acknowledgements

The authors are grateful to the anonymous reviewers for their insightful comments and feedback. The authors would also like to thank Evan Cavallo for many discussions and for his contributions of various useful results to the Cubical Agda library.

Cite As Get BibTex

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). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 11:1-11:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.CSL.2022.11

Abstract

This paper discusses the formalization of synthetic cohomology theory in a cubical extension of Agda which natively supports univalence and higher inductive types. This enables significant simplifications of many proofs from Homotopy Type Theory and Univalent Foundations as steps that used to require long calculations now hold simply by computation. To this end, we give a new definition of the group structure for cohomology with ℤ-coefficients, optimized for efficient computations. We also invent an optimized definition of the cup product which allows us to give the first complete formalization of the axioms needed to turn the integral cohomology groups into a graded commutative ring. Using this, we characterize the cohomology groups of the spheres, torus, Klein bottle and real/complex projective planes. As all proofs are constructive we can then use Cubical Agda to distinguish between spaces by computation.

Subject Classification

ACM Subject Classification
  • Theory of computation → Constructive mathematics
  • Theory of computation → Type theory
Keywords
  • Synthetic Homotopy Theory
  • Cohomology Theory
  • Cubical Agda

Metrics

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

Supplementary Materials

References

  1. Victor Alfieri. Formalisation de notions de théorie des groupes en théorie cubique des types, 2019. Internship report, supervised by Thierry Coquand. Google Scholar
  2. Carlo Angiuli, Evan Cavallo, Anders Mörtberg, and Max Zeuner. Internalizing representation independence with univalence. Proc. ACM Program. Lang., 5(POPL), January 2021. URL: https://doi.org/10.1145/3434293.
  3. Steve Awodey and Michael A. Warren. Homotopy theoretic models of identity types. Mathematical Proceedings of the Cambridge Philosophical Society, 146(1):45-55, January 2009. URL: https://doi.org/10.1017/S0305004108001783.
  4. Tim Baumann. The cup product on cohomology groups in homotopy type theory. Master’s thesis, University of Augsburg, 2018. Google Scholar
  5. Guillaume Brunerie. On the homotopy groups of spheres in homotopy type theory. PhD thesis, Université Nice Sophia Antipolis, 2016. URL: http://arxiv.org/abs/1606.05916.
  6. Guillaume Brunerie. Computer-generated proofs for the monoidal structure of the smash product. Homotopy Type Theory Electronic Seminar Talks, November 2018. URL: https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest.html.
  7. Guillaume Brunerie, Kuen-Bang Hou (Favonia), Evan Cavallo, Tim Baumann, Eric Finster, Jesper Cockx, Christian Sattler, Chris Jeris, Michael Shulman, et al. Homotopy Type Theory in Agda, 2018. URL: https://github.com/HoTT/HoTT-Agda.
  8. 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.
  9. 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.
  10. Guillaume Cano, Cyril Cohen, Maxime Dénès, Anders Mörtberg, and Vincent Siles. Formalized Linear Algebra over Elementary Divisor Rings in Coq. Logical Methods in Computer Science, 12(2), 2016. URL: https://doi.org/10.2168/LMCS-12(2:7)2016.
  11. Evan Cavallo. Synthetic Cohomology in Homotopy Type Theory. Master’s thesis, Carnegie Mellon University, 2015. Google Scholar
  12. Evan Cavallo and Robert Harper. Higher Inductive Types in Cubical Computational Type Theory. Proceedings of the ACM on Programming Languages, 3(POPL):1:1-1:27, January 2019. URL: https://doi.org/10.1145/3290314.
  13. J. Daniel Christensen and Luis Scoccola. The Hurewicz theorem in Homotopy Type Theory, 2020. Preprint. URL: http://arxiv.org/abs/2007.05833.
  14. Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. In Tarmo Uustalu, editor, 21st International Conference on Types for Proofs and Programs (TYPES 2015), volume 69 of Leibniz International Proceedings in Informatics (LIPIcs), pages 5:1-5:34, Dagstuhl, Germany, 2018. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.TYPES.2015.5.
  15. Thierry Coquand, Simon Huber, and Anders Mörtberg. On Higher Inductive Types in Cubical Type Theory. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, pages 255-264, New York, NY, USA, 2018. ACM. URL: https://doi.org/10.1145/3209108.3209197.
  16. Samuel Eilenberg and Norman Steenrod. Foundations of Algebraic Topology. Foundations of Algebraic Topology. Princeton University Press, 1952. Google Scholar
  17. Robert Graham. Synthetic Homology in Homotopy Type Theory, 2018. Preprint. URL: http://arxiv.org/abs/1706.01540.
  18. Elies Harington. Groupes de cohomologie en théorie des types univalente, 2020. Internship report, supervised by Thierry Coquand. Google Scholar
  19. Allen Hatcher. Algebraic Topology. Cambridge University Press, 2002. URL: https://pi.math.cornell.edu/~hatcher/AT/AT.pdf.
  20. Jónathan Heras, Thierry Coquand, Anders Mörtberg, and Vincent Siles. Computing Persistent Homology Within Coq/SSReflect. ACM Transactions on Computational Logic, 14(4):1-26, 2013. URL: https://doi.org/10.1145/2528929.
  21. Jónathan Heras, Maxime Dénès, Gadea Mata, Anders Mörtberg, María Poza, and Vincent Siles. Towards a Certified Computation of Homology Groups for Digital Images. In Proceedings of the 4th International Conference on Computational Topology in Image Context, CTIC'12, pages 49-57, Berlin, Heidelberg, 2012. Springer-Verlag. URL: https://doi.org/10.1007/978-3-642-30238-1_6.
  22. 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.
  23. Kuen-Bang Hou (Favonia) and Michael Shulman. The Seifert-van Kampen Theorem in Homotopy Type Theory. In Jean-Marc Talbot and Laurent Regnier, editors, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016), volume 62 of Leibniz International Proceedings in Informatics (LIPIcs), pages 22:1-22:16, Dagstuhl, Germany, 2016. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.CSL.2016.22.
  24. Krzysztof Kapulkin and Peter LeFanu Lumsdaine. The Simplicial Model of Univalent Foundations (after Voevodsky). Journal of the European Mathematical Society, 23:2071-2126, March 2021. URL: https://doi.org/10.4171/JEMS/1050.
  25. Daniel R. Licata and Guillaume Brunerie. A Cubical Approach to Synthetic Homotopy Theory. In Proceedings of the 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '15, pages 92-103, Washington, DC, USA, 2015. IEEE Computer Society. URL: https://doi.org/10.1109/LICS.2015.19.
  26. 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.
  27. 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.
  28. Axel Ljungstrröm. Computing Cohomology in Cubical Agda. Master’s thesis, Stockholm University, 2020. Google Scholar
  29. Per Martin-Löf. An Intuitionistic Theory of Types: Predicative Part. In H. E. Rose and J. C. Shepherdson, editors, Logic Colloquium '73, volume 80 of Studies in Logic and the Foundations of Mathematics, pages 73-118. North-Holland, 1975. URL: https://doi.org/10.1016/S0049-237X(08)71945-1.
  30. Per Martin-Löf. Intuitionistic type theory, volume 1 of Studies in Proof Theory. Bibliopolis, 1984. Google Scholar
  31. 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.
  32. Zesen Qian. Towards Eilenberg-MacLane Spaces in Cubical Type Theory. Master’s thesis, Carnegie Mellon University, 2019. Google Scholar
  33. Michael Shulman. Cohomology, 2013. Post on the Homotopy Type Theory blog: URL: http://homotopytypetheory.org/2013/07/24/.
  34. Kristina Sojakova. The Equivalence of the Torus and the Product of Two Circles in Homotopy Type Theory. ACM Transactions on Computational Logic, 17(4):29:1-29:19, November 2016. URL: https://doi.org/10.1145/2992783.
  35. The Agda Development Team. The Agda Programming Language, 2021. URL: http://wiki.portal.chalmers.se/agda/pmwiki.php.
  36. The Coq Development Team. The Coq Proof Assistant, 2021. URL: https://www.coq.inria.fr.
  37. The RedPRL Development Team. The cooltt proof assistant, 2021. URL: https://github.com/RedPRL/cooltt/.
  38. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. Self-published, Institute for Advanced Study, 2013. URL: https://homotopytypetheory.org/book/.
  39. Floris van Doorn. On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory. PhD thesis, Carnegie Mellon University, May 2018. URL: http://arxiv.org/abs/1808.10690.
  40. Andrea Vezzosi, Anders Mörtberg, and Andreas Abel. Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types. Proceedings of the ACM on Programming Languages, 3(ICFP):87:1-87:29, August 2019. URL: https://doi.org/10.1145/3341691.
  41. Vladimir Voevodsky. The equivalence axiom and univalent models of type theory, February 2010. Notes from a talk at Carnegie Mellon University. URL: http://www.math.ias.edu/vladimir/files/CMU_talk.pdf.
  42. Vladimir Voevodsky. An experimental library of formalized mathematics based on the univalent foundations. Mathematical Structures in Computer Science, 25(5):1278-1294, 2015. URL: https://doi.org/10.1017/S0960129514000577.
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 About DROPS Imprint Privacy Contact