Document Open Access Logo

The Formal Theory of Monads, Univalently

Author Niels van der Weide

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2023.6.pdf
  • Filesize: 0.84 MB
  • 23 pages

Document Identifiers

Author Details

Niels van der Weide
  • Institute for Computing and Information Sciences, Radboud University, Nijmegen, The Netherlands

Funding

This research was supported by the NWO project "The Power of Equality" OCENW.M20.380, which is financed by the Dutch Research Council (NWO).

Acknowledgements

The author thanks Benedikt Ahrens, Deivid Vale, Herman Geuvers, and Kobe Wullaert for their comments on earlier versions of this paper. The author also thanks the Coq developers for providing the Coq proof assistant and their continuous support to keep https://github.com/UniMath/UniMath compatible with Coq.

Cite AsGet BibTex

Niels van der Weide. The Formal Theory of Monads, Univalently. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 6:1-6:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.FSCD.2023.6

Abstract

We develop the formal theory of monads, as established by Street, in univalent foundations. This allows us to formally reason about various kinds of monads on the right level of abstraction. In particular, we define the bicategory of monads internal to a bicategory, and prove that it is univalent. We also define Eilenberg-Moore objects, and we show that both Eilenberg-Moore categories and Kleisli categories give rise to Eilenberg-Moore objects. Finally, we relate monads and adjunctions in arbitrary bicategories. Our work is formalized in Coq using the https://github.com/UniMath/UniMath library.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Type theory
Keywords
  • bicategory theory
  • univalent foundations
  • formalization
  • monads
  • Coq

Metrics

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

Related Versions

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, pages 1-38, 2022. URL: https://doi.org/10.1017/S0960129522000032.
  2. 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.
  3. Benedikt Ahrens and Peter LeFanu Lumsdaine. Displayed Categories. Logical Methods in Computer Science, 15(1), 2019. URL: https://doi.org/10.23638/LMCS-15(1:20)2019.
  4. Benedikt Ahrens, Ralph Matthes, and Anders Mörtberg. From Signatures to Monads in UniMath. J. Autom. Reason., 63(2):285-318, 2019. URL: https://doi.org/10.1007/s10817-018-9474-4.
  5. Benedikt Ahrens, Ralph Matthes, and Anders Mörtberg. Implementing a category-theoretic framework for typed abstract syntax. In Andrei Popescu and Steve Zdancewic, editors, CPP '22: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022, pages 307-323. ACM, 2022. URL: https://doi.org/10.1145/3497775.3503678.
  6. Benedikt Ahrens, Paige Randall North, Michael Shulman, and Dimitris Tsementzis. The univalence principle. CoRR, abs/2102.06275, 2021. URL: https://arxiv.org/abs/2102.06275.
  7. Benedikt Ahrens, Paige Randall North, and Niels van der Weide. Semantics for two-dimensional type theory. CoRR, abs/2201.10662, 2022. URL: https://arxiv.org/abs/2201.10662.
  8. Nathanael Arkor and Dylan McDermott. The formal theory of relative monads. arXiv preprint arXiv:2302.14014, 2023. Google Scholar
  9. 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 Yves Bertot and Viktor Vafeiadis, editors, Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017, pages 164-172. ACM, 2017. URL: https://doi.org/10.1145/3018610.3018615.
  10. Jean Bénabou. Introduction to bicategories. In Reports of the Midwest Category Seminar, pages 1-77, Berlin, Heidelberg, 1967. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/BFb0074299.
  11. P. N. Benton. A mixed linear and non-linear logic: Proofs, terms and models (extended abstract). In Leszek Pacholski and Jerzy Tiuryn, editors, Computer Science Logic, 8th International Workshop, CSL '94, Kazimierz, Poland, September 25-30, 1994, Selected Papers, volume 933 of Lecture Notes in Computer Science, pages 121-135. Springer, 1994. URL: https://doi.org/10.1007/BFb0022251.
  12. Gabriella Böhm, Stephen Lack, and Ross Street. On the 2-categories of weak distributive laws. Communications in Algebra, 39(12):4567-4583, 2011. Google Scholar
  13. Matteo Capucci and Bruno Gavranović. Actegories for the Working Amthematician. arXiv preprint arXiv:2203.16351, 2022. Google Scholar
  14. Eugenia Cheng. Iterated distributive laws. Mathematical Proceedings of the Cambridge Philosophical Society, 150(3):459-487, 2011. Google Scholar
  15. Ivan Di Liberti and Fosco Loregian. On the unicity of formal category theories. arXiv preprint arXiv:1901.01594, 2019. Google Scholar
  16. Jeff Egger, Rasmus Ejlers Møgelberg, and Alex Simpson. The enriched effect calculus: syntax and semantics. J. Log. Comput., 24(3):615-654, 2014. URL: https://doi.org/10.1093/logcom/exs025.
  17. Soichiro Fujii, Shin-ya Katsumata, and Paul-André Melliès. Towards a Formal Theory of Graded Monads. In Bart Jacobs and Christof Löding, editors, Foundations of Software Science and Computation Structures - 19th International Conference, FOSSACS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, volume 9634 of Lecture Notes in Computer Science, pages 513-530. Springer, 2016. URL: https://doi.org/10.1007/978-3-662-49630-5_30.
  18. 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 - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, volume 8558 of Lecture Notes in Computer Science, pages 275-291. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-08970-6_18.
  19. 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.
  20. Martin Hyland and John Power. The category theoretic understanding of universal algebra: Lawvere theories and monads. Electronic Notes in Theoretical Computer Science, 172:437-458, 2007. Google Scholar
  21. Niles Johnson and Donald Yau. 2-dimensional categories. Oxford University Press, USA, 2021. Google Scholar
  22. Simon L. Peyton Jones and Philip Wadler. Imperative Functional Programming. In Mary S. Van Deusen and Bernard Lang, editors, Conference Record of the Twentieth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Charleston, South Carolina, USA, January 1993, pages 71-84. ACM Press, 1993. URL: https://doi.org/10.1145/158511.158524.
  23. Krzysztof Kapulkin and Peter LeFanu Lumsdaine. The Simplicial Model of Univalent Foundations (after Voevodsky). Journal of the European Mathematical Society, 23(6):2071-2126, 2021. URL: https://doi.org/10.4171/JEMS/1050.
  24. Gregory Maxwell Kelly. Elementary observations on 2-categorical limits. Bulletin of the Australian Mathematical Society, 39(2):301-317, 1989. Google Scholar
  25. Max Kelly. Basic concepts of enriched category theory, volume 64. CUP Archive, 1982. Google Scholar
  26. Stephen Lack. Composing props. Theory and Applications of Categories, 13(9):147-163, 2004. Google Scholar
  27. Stephen Lack. A 2-categories companion. In Towards higher categories, pages 105-191. Springer, 2010. Google Scholar
  28. Stephen Lack and Ross Street. The formal theory of monads II. Journal of pure and applied algebra, 175(1-3):243-265, 2002. Google Scholar
  29. Tom Leinster. Basic Bicategories, 1998. URL: https://arxiv.org/abs/math/9810017.
  30. Paul Blain Levy. Call-by-push-value: A Functional/imperative Synthesis, volume 2. Springer Science & Business Media, 2012. Google Scholar
  31. Saunders Mac Lane. Categories for the working mathematician, volume 5. Springer Science & Business Media, 2013. Google Scholar
  32. Saunders MacLane and Robert Paré. Coherence for bicategories and indexed categories. Journal of Pure and Applied Algebra, 37:59-80, 1985. Google Scholar
  33. The mathlib Community. The Lean mathematical library. In Jasmin Blanchette and Catalin Hritcu, editors, Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020, pages 367-381. ACM, 2020. URL: https://doi.org/10.1145/3372885.3373824.
  34. Paul-André Mellies. Categorical semantics of linear logic. Panoramas et syntheses, 27:15-215, 2009. Google Scholar
  35. Eugenio Moggi. Computational lambda-calculus and monads. In Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS '89), Pacific Grove, California, USA, June 5-8, 1989, pages 14-23. IEEE Computer Society, 1989. URL: https://doi.org/10.1109/LICS.1989.39155.
  36. Eugenio Moggi. Notions of computation and monads. Information and computation, 93(1):55-92, 1991. Google Scholar
  37. Tobias Nipkow, Lawrence C Paulson, and Markus Wenzel. Isabelle/HOL: a proof assistant for higher-order logic, volume 2283. Springer Science & Business Media, 2002. Google Scholar
  38. Ulf Norell. Dependently typed programming in Agda. In Proceedings of the 4th international workshop on Types in language design and implementation, pages 1-2, 2009. Google Scholar
  39. Gordon Plotkin and John Power. Notions of computation determine monads. In International Conference on Foundations of Software Science and Computation Structures, pages 342-356. Springer, 2002. Google Scholar
  40. Gordon Plotkin and John Power. Algebraic operations and generic effects. Applied categorical structures, 11(1):69-94, 2003. Google Scholar
  41. John Power. Coherence for bicategories with finite bilimits I. In Categories in computer science and logic, volume 92 of Contemporary Mathematics, pages 341-347, 1989. Google Scholar
  42. John Power. Enriched Lawvere theories. Theory and Applications of Categories, 6(7):83-93, 1999. Google Scholar
  43. John Power and Edmund Robinson. A Characterization of PIE Limits. Mathematical Proceedings of the Cambridge Philosophical Society, 110:33-47, 1991. Google Scholar
  44. John Power and Hiroshi Watanabe. Combining a monad and a comonad. Theoretical Computer Science, 280(1-2):137-162, 2002. Google Scholar
  45. Egbert Rijke, Elisabeth Bonnevier, Jonathan Prieto-Cubides, et al. Univalent mathematics in Agda. https://unimath.github.io/agda-unimath/. URL: https://github.com/UniMath/agda-unimath/.
  46. Eugene W. Stark. Bicategories. Arch. Formal Proofs, 2020, 2020. URL: https://www.isa-afp.org/entries/Bicategory.html.
  47. Ross Street. The formal theory of monads. Journal of Pure and Applied Algebra, 2(2):149-168, 1972. Google Scholar
  48. The Coq Development Team. The Coq Proof Assistant, September 2022. URL: https://doi.org/10.5281/zenodo.7313584.
  49. The 1Lab Development Team. The 1Lab. URL: https://1lab.dev.
  50. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
  51. 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://lmcs.episciences.org/7391.
  52. Andrea Vezzosi, Anders Mörtberg, and Andreas Abel. Cubical Agda: a dependently typed programming language with univalence and higher inductive types. Proc. ACM Program. Lang., 3(ICFP):87:1-87:29, 2019. URL: https://doi.org/10.1145/3341691.
  53. 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.7848572.
  54. Kobe Wullaert, Ralph Matthes, and Benedikt Ahrens. Univalent monoidal categories. arXiv preprint arXiv:2212.03146, 2022. 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
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact