Insights from Univalent Foundations: A Case Study Using Double Categories

Authors Nima Rasekh , Niels van der Weide , Benedikt Ahrens , Paige Randall North



PDF
Thumbnail PDF

File

LIPIcs.CSL.2025.45.pdf
  • Filesize: 0.81 MB
  • 18 pages

Document Identifiers

Author Details

Nima Rasekh
  • Institute of Mathematics and Computer Science, University of Greifswald, Germany
Niels van der Weide
  • Institute for Computing and Information Sciences, Radboud University, Nijmegen, The Netherlands
Benedikt Ahrens
  • Delft University of Technology, The Netherlands
  • University of Birmingham, UK
Paige Randall North
  • Department of Information and Computing Sciences and Mathematical Institute, Utrecht University, The Netherlands

Acknowledgements

We gratefully acknowledge the work by the Coq development team in providing the Coq proof assistant and surrounding infrastructure, as well as their support in keeping UniMath compatible with Coq. We are very grateful to Mike Shulman for answering our questions about profunctors. We would also like to thank Lyne Moser for many valuable discussions and explanations regarding double categories, their equivalences, and important references. The first author is grateful to the Max Planck Institute for Mathematics in Bonn for its hospitality and financial support.

Cite As Get BibTex

Nima Rasekh, Niels van der Weide, Benedikt Ahrens, and Paige Randall North. Insights from Univalent Foundations: A Case Study Using Double Categories. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 45:1-45:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CSL.2025.45

Abstract

Category theory unifies mathematical concepts, aiding comparisons across structures by incorporating not just objects, but also morphisms capturing interactions between objects. Of particular importance in some applications are double categories, which are categories with two classes of morphisms, axiomatizing two different kinds of interactions between objects. These have found applications in many areas of mathematics and theoretical computer science, for instance, the study of lenses, open systems, and rewriting.
However, double categories come with a wide variety of equivalences, which makes it challenging to transport structure along equivalences. To deal with this challenge, we propose the univalence maxim: each notion of equivalence of categorical structures has a corresponding notion of univalent categorical structure which induces that notion of equivalence. We also prove corresponding univalence principles, which allow us to transport structure and properties along equivalences. In this way, the usually informal practice of reasoning modulo equivalence becomes grounded in an entirely formal logical principle.
We apply this perspective to various double categorical structures, such as (pseudo) double categories and double bicategories. Concretely, we characterize and formalize their definitions in Coq UniMath up to chosen equivalences, which we achieve by establishing their univalence principles.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Type theory
Keywords
  • formalization of mathematics
  • category theory
  • double categories
  • univalent foundations

Metrics

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

References

  1. Samson Abramsky and Steven Vickers. Quantales, observational logic and process semantics. Math. Structures Comput. Sci., 3(2):161-227, 1993. URL: https://doi.org/10.1017/S0960129500000189.
  2. Benedikt Ahrens, Dan Frumin, Marco Maggesi, Niccolò Veltri, and Niels van der Weide. Bicategories in univalent foundations. Math. Struct. Comput. Sci., 31(10):1232-1269, 2021. URL: https://doi.org/10.1017/S0960129522000032.
  3. Benedikt Ahrens, Krzysztof Kapulkin, and Michael Shulman. Univalent categories and the Rezk completion. Mathematical Structures in Computer Science, 25:1010-1039, 2015. URL: https://doi.org/10.1017/S0960129514000486.
  4. Benedikt Ahrens, Paige Randall North, Michael Shulman, and Dimitris Tsementzis. The Univalence Principle, 2022. To be published in Mem. AMS. URL: https://arxiv.org/abs/2102.06275v3.
  5. Steve Awodey. Natural models of homotopy type theory. Math. Struct. Comput. Sci., 28(2):241-286, 2018. URL: https://doi.org/10.1017/S0960129516000268.
  6. John C. Baez and Kenny Courser. Structured cospans. Theory Appl. Categ., 35:Paper No. 48, 1771-1822, 2020. Google Scholar
  7. John C. Baez, Kenny Courser, and Christina Vasilakopoulou. Structured versus Decorated Cospans. Compositionality, 4, September 2022. URL: https://doi.org/10.32408/compositionality-4-3.
  8. Nicolas Behr, Russ Harmer, and Jean Krivine. Fundamentals of compositional rewriting theory. J. Log. Algebraic Methods Program., 135:100893, 2023. URL: https://doi.org/10.1016/J.JLAMP.2023.100893.
  9. Nicolas Behr, Paul-André Melliès, and Noam Zeilberger. Convolution products on double categories and categorification of rule algebras. In Marco Gaboardi and Femke van Raamsdonk, editors, 8th International Conference on Formal Structures for Computation and Deduction, FSCD 2023, July 3-6, 2023, Rome, Italy, volume 260 of LIPIcs, pages 17:1-17:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPICS.FSCD.2023.17.
  10. Georges Blanc. Équivalence naturelle et formules logiques en théorie des catégories. Arch. Math. Logik Grundlag., 19(3-4):131-137, 1978. URL: https://doi.org/10.1007/BF02011874.
  11. Guillaume Boisseau and Jeremy Gibbons. What you needa know about yoneda: profunctor optics and the yoneda lemma (functional pearl). Proc. ACM Program. Lang., 2(ICFP):84:1-84:27, 2018. URL: https://doi.org/10.1145/3236779.
  12. Simon Castellan, Pierre Clairambault, and Peter Dybjer. Categories with families: Unityped, simply typed, and dependently typed. In Joachim Lambek: The Interplay of Mathematics, Logic, and Linguistics, volume 20 of Outst. Contrib. Log., pages 135-180. Springer, Cham, 2021. URL: https://doi.org/10.1007/978-3-030-66545-6_5.
  13. Bryce Clarke, Derek Elkins, Jeremy Gibbons, Fosco Loregiàn, Bartosz Milewski, Emily Pillmore, and Mario Román. Profunctor optics, a categorical update. CoRR, abs/2001.07488, 2020. URL: https://arxiv.org/abs/2001.07488.
  14. Pierre-Évariste Dagand and Conor McBride. A categorical treatment of ornaments. In 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, USA, June 25-28, 2013, pages 530-539. IEEE Computer Society, 2013. URL: https://doi.org/10.1109/LICS.2013.60.
  15. Fredrik Dahlqvist and Renato Neves. An internal language for categories enriched over generalised metric spaces. In 30th EACSL Annual Conference on Computer Science Logic, volume 216 of LIPIcs. Leibniz Int. Proc. Inform., pages Art. No. 16, 18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.CSL.2022.16.
  16. Charles Ehresmann. Catégories structurées. III. Quintettes et applications covariantes. In Topol. et Géom. Diff. (Sém. C. Ehresmann), Vol. V, volume Vol. V of Cahiers du Séminaire dirigé par Charles Ehresmann, page 21. Inst. Henri Poincaré, Paris, 1963. Google Scholar
  17. P. Freyd. Properties invariant within equivalence types of categories. In A. Heller and M. Tierney, editors, Algebra, Topology and Category Theory: A Collection of Papers in Honor of Samuel Eilenberg, pages 55-61. Academic Press, New York, 1976. Google Scholar
  18. Dennis Gaitsgory and Nick Rozenblyum. A study in derived algebraic geometry. Vol. II. Deformations, Lie theory and formal geometry, volume 221 of Mathematical Surveys and Monographs. American Mathematical Society, Providence, RI, 2017. URL: https://doi.org/10.1090/surv/221.2.
  19. R. Gordon, A. J. Power, and Ross Street. Coherence for tricategories. Mem. Amer. Math. Soc., 117(558):vi+81, 1995. URL: https://doi.org/10.1090/memo/0558.
  20. Marco Grandis and Robert Pare. Limits in double categories. Cahiers Topologie Géom. Différentielle Catég., 40(3):162-220, 1999. Google Scholar
  21. Marco Grandis and Robert Pare. Adjoint for double categories. Addenda to: "Limits in double categories" [Cah. Topol. Géom. Différ. Catég. 40 (1999), no. 3, 162-220; mr1716779]. Cah. Topol. Géom. Différ. Catég., 45(3):193-240, 2004. Google Scholar
  22. Jason Z. S. Hu and Jacques Carette. Formalizing category theory in agda. In Catalin Hritcu and Andrei Popescu, editors, CPP '21: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021, pages 327-342. ACM, 2021. URL: https://doi.org/10.1145/3437992.3439922.
  23. G. M. Kelly and Ross Street. Review of the elements of 2-categories. In Category Seminar (Proc. Sem., Sydney, 1972/1973), volume Vol. 420 of Lecture Notes in Math., pages 75-103. Springer, Berlin-New York, 1974. Google Scholar
  24. Michael Makkai. First order logic with dependent sorts, with applications to category theory, 1995. URL: http://www.math.mcgill.ca/makkai/folds/foldsinpdf/FOLDS.pdf.
  25. Jeffrey C. Morton. Double bicategories and double cospans. J. Homotopy Relat. Struct., 4(1):389-428, 2009. Google Scholar
  26. Lyne Moser, Maru Sarazola, and Paula Verdugo. A model structure for weakly horizontally invariant double categories. Algebr. Geom. Topol., 23(4):1725-1786, 2023. URL: https://doi.org/10.2140/agt.2023.23.1725.
  27. Zach Murray, Dorette Pronk, and Martin Szyld. Implementing double categories in the lean proof assistant, 2022. Talk at Science Atlantic Mathematics, Statistics, and Computer Science Conference, October 15, 2022. URL: https://www.mathstat.dal.ca/~mszyld/Zach_slides.pdf.
  28. Max S. New and Daniel R. Licata. Call-by-name gradual type theory. Log. Methods Comput. Sci., 16(1), 2020. URL: https://doi.org/10.23638/LMCS-16(1:7)2020.
  29. Max S. New and Daniel R. Licata. A formal logic for formal category theory. In Orna Kupferman and Pawel Sobocinski, editors, Foundations of Software Science and Computation Structures - 26th International Conference, FoSSaCS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22-27, 2023, Proceedings, volume 13992 of Lecture Notes in Computer Science, pages 113-134. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-30829-1_6.
  30. Kimmo I. Rosenthal. Quantaloids, enriched categories and automata theory. Appl. Categ. Structures, 3(3):279-301, 1995. URL: https://doi.org/10.1007/BF00878445.
  31. Michael Shulman. Framed bicategories and monoidal fibrations. Theory Appl. Categ., 20:No. 18, 650-738, 2008. Google Scholar
  32. The 1Lab Development Team. The 1Lab. URL: https://1lab.dev.
  33. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
  34. Niels van der Weide, Nima Rasekh, Benedikt Ahrens, and Paige Randall North. Univalent double categories. In Amin Timany, Dmitriy Traytel, Brigitte Pientka, and Sandrine Blazy, editors, Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2024, London, UK, January 15-16, 2024, pages 246-259. ACM, 2024. URL: https://doi.org/10.1145/3636501.3636955.
  35. Dominic Verity. Enriched categories, internal categories and change of base. Repr. Theory Appl. Categ., 20:1-266, 2011. Google Scholar
  36. Vladimir Voevodsky, Benedikt Ahrens, Daniel Grayson, et al. Unimath - a computer-checked library of univalent mathematics. available at http://unimath.org. URL: https://doi.org/10.5281/zenodo.13828995.
  37. R. J. Wood. Abstract proarrows. I. Cahiers Topologie Géom. Différentielle, 23(3):279-290, 1982. Google Scholar
  38. R. J. Wood. Proarrows. II. Cahiers Topologie Géom. Différentielle Catég., 26(2):135-168, 1985. Google Scholar
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