Document Open Access Logo

Formalizing Colimits in 𝒞at

Authors Mario Carneiro , Emily Riehl

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.ITP.2025.20.pdf
  • Filesize: 1.97 MB
  • 19 pages
HTML5 Logo HTML (experimental)
LIPIcs.ITP.2025.20.html

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • category theory
  • infinity-category theory
  • nerve
  • simplicial set
  • colimit

Metrics

Abstract

Certain results involving "higher structures" are not currently accessible to computer formalization because the prerequisite ∞-category theory has not been formalized. To support future work on formalizing ∞-category theory in Lean’s mathematics library, we formalize some fundamental constructions involving the 1-category of categories. Specifically, we construct the left adjoint to the nerve embedding of categories into simplicial sets, defining the homotopy category functor. We prove further that this adjunction is reflective, which allows us to conclude that 𝒞at has colimits. To our knowledge this is the first formalized proof that the nerve functor is a fully faithful right adjoint and that the category of categories is cocomplete.

Cite As Get BibTex

Mario Carneiro and Emily Riehl. Formalizing Colimits in 𝒞at. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 20:1-20:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.ITP.2025.20

Author Details

Mario Carneiro
  • Chalmers University of Technology, Gothenburg, Sweden
Emily Riehl
  • Department of Mathematics, Johns Hopkins University, Baltimore, MD, USA

Funding

  • Riehl, Emily: NSF DMS-2204304, AFOSR FA9550-21-1-0009, ARO W911NF-20-1-0082.

Acknowledgements

This project was first instantiated at the 2024 Prospects of Formal Mathematics Trimester Program at the Hausdorff Institute for Mathematics in Bonn. The authors are grateful to the organizers of that program for facilitating many new collaborations and to the HIM for its hospitality. They also wish to thank Joël Riou for the excellent suggestions he made during the Mathlib PR review process. The final journal version contains myriad expository improvements suggested by the reviewers.

Supplementary Materials

References

  1. J. Adamek and J. Rosicky. Locally Presentable and Accessible Categories. London Mathematical Society Lecture Note Series. Cambridge University Press, 1994. Google Scholar
  2. Benedikt Ahrens, Krzysztof Kapulkin, and Michael Shulman. Univalent categories and the rezk completion. Mathematical Structures in Computer Science, 25(5):1010-1039, 2015. URL: https://doi.org/10.1017/S0960129514000486.
  3. Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, and Bas Spitters. The HoTT library: A formalization of homotopy type theory in Coq. In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, pages 164-172, New York, NY, USA, 2017. Association for Computing Machinery. URL: https://doi.org/10.1145/3018610.3018615.
  4. Marek A. Bednarczyk, Andrzej M. Borzyszkowski, and Wieslaw Pawlowski. Generalized congruences - Epimorphisms in Cat. Theory and Applications of Categories, 5(11):266-280, 1999. Google Scholar
  5. A.J. Blumberg, D. Gepner, and G. Tabuada. A universal characterization of higher algebraic k-theory. Geometry & Topology, 2(17):733-838, 2013. URL: https://doi.org/10.2140/gt.2013.17.733.
  6. Francis Borceux. Handbook of Categorical Algebra 1: Basic Category Theory. Encyclopedia of Mathematics and its Applications. Cambridge University Press, 1994. Google Scholar
  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. https://github.com/HoTT/HoTT-Agda, 2019.
  8. Mario Carneiro, Emily Riehl, and Dominic Verity. The ∞-cosmos project. https://emilyriehl.github.io/infinity-cosmos/, 2025.
  9. Eduardo Dubuc. Adjoint triangles. In S. MacLane, editor, Reports of the Midwest Category Seminar II, pages 69-91, Berlin, Heidelberg, 1968. Springer Berlin Heidelberg. Google Scholar
  10. L. Fargues and P. Scholze. Geometrization of the local Langlands correspondence. arXiv:2102.13459, 2024. Google Scholar
  11. P.G. Goerss and J.F. Jardine. Simplicial homotopy theory. Birkhäuser Basel, 2009. Google Scholar
  12. Jason Gross, Adam Chlipala, and David I. Spivak. Experience implementing a performant category-theory library in coq. In Gerwin Klein and Ruben Gamboa, editors, Interactive Theorem Proving, pages 275-291, Cham, 2014. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-08970-6_18.
  13. John Harrison. Formalized mathematics. Technical Report 36, Turku Centre for Computer Science (TUCS), 1996. URL: http://www.cl.cam.ac.uk/~jrh13/papers/form-math3.html.
  14. John Harrison. Hol light: An overview. In International Conference on Theorem Proving in Higher Order Logics, pages 60-66. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-03359-9_4.
  15. Jason Z. S. Hu and Jacques Carette. Formalizing category theory in Agda. In Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2021, pages 327-342, New York, NY, USA, 2021. Association for Computing Machinery. URL: https://doi.org/10.1145/3437992.3439922.
  16. Gérard Huet and Amokrane Saïbi. Constructive category theory. In Proof, Language, and Interaction: Essays in Honour of Robin Milner. The MIT Press, May 2000. URL: https://doi.org/10.7551/mitpress/5641.003.0015.
  17. S. A. Huq. An interpolation theorem for adjoint functors. Proc. Amer. Math. Soc., 25:880-883, 1970. URL: https://doi.org/10.1090/S0002-9939-1970-0260824-1.
  18. Nikolai Kudasov, Emily Riehl, and Jonathan Weinberger. Formalizing the ∞-categorical Yoneda lemma. In Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2024, pages 274-290, New York, NY, USA, 2024. Association for Computing Machinery. URL: https://doi.org/10.1145/3636501.3636945.
  19. Amélia Liao, Daniel Sölch, Jonathan Coates, Matthew McQuaid, Nathan van Doorn, Naïm Favier, Patrick Nicodemus, Reed Mullanix, favonia, uni, et al. 1Lab. https://1lab.dev/, 2025.
  20. J. Lurie. Spectral Algebraic Geometry. www.math.ias.edu/∼lurie/papers/SAG-rootfile.pdf, February 2018. Google Scholar
  21. Jacob Lurie. Derived algebraic geometry. PhD thesis, Massachusetts Institute of Technology, 2004. URL: http://hdl.handle.net/1721.1/30144.
  22. S. Mac Lane. Categories for the Working Mathematician. Graduate Texts in Mathematics. Springer-Verlag, second edition, 1998. Google Scholar
  23. The mathlib Community. The lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, pages 367-381, New York, NY, USA, 2020. Association for Computing Machinery. URL: https://doi.org/10.1145/3372885.3373824.
  24. Mihails Milehins. Category theory for ZFC in HOL I: Foundations: Design patterns, set theory, digraphs, semicategories. Archive of Formal Proofs, September 2021. , Formal proof development. URL: https://isa-afp.org/entries/CZH_Foundations.html.
  25. Mihails Milehins. Category theory for ZFC in HOL II: Elementary theory of 1-categories. Archive of Formal Proofs, September 2021. , Formal proof development. URL: https://isa-afp.org/entries/CZH_Elementary_Categories.html.
  26. Mihails Milehins. Category theory for ZFC in HOL III: Universal constructions. Archive of Formal Proofs, September 2021. , Formal proof development. URL: https://isa-afp.org/entries/CZH_Universal_Constructions.html.
  27. Kim Morrison. Lean category theory. https://github.com/kim-em/lean-category-theory, 2023.
  28. David Nadler and Hiro Lee Tanaka. A stable ∞-category of Lagrangian cobordisms. Advances in Mathematics, 366:107026, 2020. URL: https://doi.org/10.1016/j.aim.2020.107026.
  29. Tobias Nipkow, Markus Wenzel, and Lawrence C Paulson. Isabelle/HOL: a proof assistant for higher-order logic. Springer, 2002. URL: https://doi.org/10.1007/3-540-45949-9.
  30. Greg O'Keefe. Towards a readable formalisation of category theory. Electronic Notes in Theoretical Computer Science, 91:212-228, 2004. Proceedings of Computing: The Australasian Theory Symposium (CATS) 2004. URL: https://doi.org/10.1016/j.entcs.2003.12.014.
  31. C.L. Reedy. Homotopy theory of model categories. unpublished manuscript. URL: https://math.mit.edu/~psh/reedy.pdf.
  32. Emily Riehl. Category Theory in Context. Aurora Modern Math Originals. Dover Publications, 2016. Google Scholar
  33. Emily Riehl and Dominic Verity. Elements of ∞-Category Theory. Cambridge Studies in Advanced Mathematics. Cambridge University Press, 2022. Google Scholar
  34. Egbert Rijke, Elisabeth Bonnevier, Jonathan Prieto-Cubides, Fredrik Bakke, et al. The agda-unimath library, 2025. URL: https://github.com/UniMath/agda-unimath/.
  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. Vladimir Voevodsky, Benedikt Ahrens, Daniel Grayson, et al. Unimath - a computer-checked library of univalent mathematics. URL: https://doi.org/10.5281/zenodo.7848572.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact