Document Open Access Logo

String Diagrams for Monoidal Categories, in Rocq

Author Damien Pous

PDF

File

Thumbnail PDF
PDF
LIPIcs.ITP.2026.28.pdf
  • Filesize: 0.77 MB
  • 20 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic
Keywords
  • Monoidal categories
  • string diagrams
  • formal proofs
  • graphical proofs
  • Rocq

Metrics

Abstract

We present a Rocq library for monoidal categories, including a decision procedure for proving equality of morphisms as well as notations that make it possible to reason as if these monoidal categories were strict, inferring MacLane isomorphims automatically in the background. Together with an external tool for visualising and editing string diagrams, this make it possible to perform rewriting steps graphically, and to translate them into textual formal proofs which are concise and readable.

Cite As Get BibTex

Damien Pous. String Diagrams for Monoidal Categories, in Rocq. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 28:1-28:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.ITP.2026.28

Author Details

Damien Pous
  • Plume team, CNRS, LIP, ENS de Lyon, UMR 5668, France

Acknowledgements

We are grateful to Ralph Sarkis for two seminars he gave in 2023 to the Plume team, where he advocated the use of (string) diagrammatic proofs and showed us the proofs for monoid composition we use as a running example in the present paper.

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, 31(10):1232-1269, 2021. URL: https://doi.org/10.1017/S0960129522000032.
  2. Clément Allain, Basile Clément, Alexandre Moine, and Gabriel Scherer. Snapshottable stores. Proc. ACM Program. Lang., 8(ICFP), 2024. URL: https://doi.org/10.1145/3674637.
  3. Samuel Arsac, Russ Harmer, and Damien Pous. Adhesive category theory for graph rewriting in Rocq. In Proc. CPP, pages 59-74. ACM, 2026. URL: https://doi.org/10.1145/3779031.3779105.
  4. Krzysztof Bar, Aleks Kissinger, and Jamie Vicary. Globular: An Online Proof Assistant for Higher-Dimensional Rewriting. In Proc. FSCD, volume 52 of LIPIcs, pages 34:1-34:11. Schloss Dagstuhl, 2016. URL: https://doi.org/10.4230/LIPIcs.FSCD.2016.34.
  5. Ilya Beylin and Peter Dybjer. Extracting a proof of coherence for monoidal categories from a proof of normalization for monoids. In Proc. TYPES, selected Papers, volume 1158 of LNCS, pages 47-61. Springer, 1995. URL: https://doi.org/10.1007/3-540-61780-9_61.
  6. Filippo Bonchi, Fabio Gadducci, Aleks Kissinger, Pawel Sobocinski, and Fabio Zanasi. String diagram rewrite theory II: Rewriting with symmetric monoidal structure. Mathematical Structures in Computer Science, 32(4):511-541, 2022. URL: https://doi.org/10.1017/S0960129522000317.
  7. Francis Borceux. Handbook of Categorical Algebra: Volume 1: Basic Category Theory. Encyclopedia of Mathematics and Its Applications. Cambridge University Press, 1994. URL: https://doi.org/10.1017/CBO9780511525858.
  8. Samuel Boutin. Using reflection to build efficient and certified decision procedures. In Proc. TACS, pages 515-529. Springer, 1997. URL: https://doi.org/10.5555/645869.668533.
  9. Jean Bénabou. Catégories avec multiplication. Compte rendus de l'académie des sciences, 256, 1963. Google Scholar
  10. Jean Bénabou. Les catégories multiplicatives. Séminaire de mathématique pure, 27, 1972. URL: https://ncatlab.org/nlab/files/Benabou-CategoriesMultiplicatives.pdf.
  11. Daniel Bünzli. Vector graphic, 2013. URL: https://erratique.ch/software/vg.
  12. Luc Chabassier. Aspects of Category Theory in Proof Assistants. Thèse de doctorat, Université Paris-Saclay, July 2025. URL: https://theses.fr/2025UPASG055.
  13. Luc Chabassier. A Graphical Interface for Category Theory Proofs in Coq. Electronic Proceedings in Theoretical Computer Science, pages 28-41, 2025. URL: https://doi.org/10.4204/EPTCS.419.2.
  14. Cyril Cohen, Kazuhiko Sakaguchi, and Enrico Tassi. Hierarchy Builder: Algebraic hierarchies made easy in Coq with Elpi. In Proc. FSCD, pages 34:1-34:21, 2020. URL: https://doi.org/10.4230/LIPIcs.FSCD.2020.34.
  15. Nathan Corbyn, Lukas Heidemann, Nick Hu, Chiara Sarti, Calin Tataru, and Jamie Vicary. homotopy.io: A Proof Assistant for Finitely-Presented Globular n-Categories. In Proc. FSCD, volume 299 of LIPIcs, pages 30:1-30:26. Schloss Dagstuhl, 2024. URL: https://doi.org/10.4230/LIPIcs.FSCD.2024.30.
  16. Cvetan Dunchev, Ferruccio Guidi, Claudio Sacerdoti Coen, and Enrico Tassi. ELPI: fast, embeddable, λprolog interpreter. In Proc. LPAR, LNCS, pages 460-468. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-48899-7_32.
  17. Samuel Eilenberg and Max Kelly. Closed categories. In Proceedings of the Conference on Categorical Algebra, pages 421-562. Springer, 1966. Section II.1. URL: https://doi.org/10.1007/978-3-642-99902-4.
  18. Sam Ezeh. Graphical Rewriting for Diagrammatic Reasoning in Monoidal Categories in Lean4. In Proc. ITP, volume 309 of LIPIcs, pages 41:1-41:8. Schloss Dagstuhl, 2024. URL: https://doi.org/10.4230/LIPIcs.ITP.2024.41.
  19. François Garillot, Georges Gonthier, Assia Mahboubi, and Laurence Rideau. Packaging Mathematical Structures. In Proc. TPHOLs, pages 327-342, 2009. URL: https://doi.org/10.1007/978-3-642-03359-9_23.
  20. Benjamin Grégoire and Assia Mahboubi. Proving equalities in a commutative ring done right in Coq. In Proc. TPHOL, volume 3603 of LNCS, pages 98-113. Springer, 2005. URL: https://doi.org/10.1007/11541868_7.
  21. Günter Hotz. Eine algebraisierung des syntheseproblems von schaltkreisen. EIK, Bd. 1, (185-205), Bd, 2, (209-231), 1965. Google Scholar
  22. André Joyal and Ross Street. The geometry of tensor calculus, I. Advances in Mathematics, 88(1):55-112, 1991. URL: https://doi.org/10.1016/0001-8708(91)90003-P.
  23. Max Kelly. On MacLane’s conditions for coherence of natural associativities, commutativities, etc. Journal of Algebra, 1:397-402, 1964. Google Scholar
  24. Max Kelly. Many-variable functorial calculus. I. In Coherence in Categories, pages 66-105. Springer, 1972. URL: https://doi.org/10.1007/BFb0059556.
  25. Yoshiki Kinoshita. A bicategorical analysis of e-categories, February 1997. URL: https://www.researchgate.net/publication/2710125_A_bicategorical_analysis_of_E-categories.
  26. Aleks Kissinger. Chyp, 2023. URL: https://github.com/akissinger/chyp.
  27. Aleks Kissinger and Vladimir Zamdzhiev. Quantomatic: A proof assistant for diagrammatic reasoning. In Proc. CADE, pages 326-336, 2015. Google Scholar
  28. Ambroise Lafont. A diagram editor to mechanise categorical proofs. In Proc. JFLA, 2024. URL: https://hal.science/hal-04407118.
  29. Saunders Mac Lane. Natural associativity and commutativity. Rice University Studies, 49:28-46, 1963. Google Scholar
  30. Adrian Lehmann, Ben Caldwell, Bhakti Shah, William Spencer, and Robert Rand. VyZX: Formal verification of a graphical quantum language. ACM Transactions on Programming Languages and Systems, April 2026. Just Accepted. URL: https://doi.org/10.1145/3807780.
  31. Meven Lennon-Bertrand. Complete bidirectional typing for the calculus of inductive constructions. In Proc. ITP, LIPIcs, pages 24:1-24:19. Schloss Dagstuhl, 2021. URL: https://doi.org/10.4230/LIPIcs.ITP.2021.24.
  32. Saunders Mac Lane. Categories for the Working Mathematician. Graduate texts in mathematics 5. Springer, 2nd ed., reprint edition, 1971 - 1998. Google Scholar
  33. Roger Penrose. Applications of negative dimensional tensors. Combinatorial Mathematics and its Applications, 1971. Google Scholar
  34. Roger Penrose and Wolfgang Rindler. Spinors and Space-Time. Cambridge Monographs on Mathematical Physics. Cambridge University Press, 1984. URL: https://doi.org/10.1017/CBO9780511564048.
  35. Robin Piedeleu and Fabio Zanasi. An Introduction to String Diagrams for Computer Scientists. Elements in Applied Category Theory. Cambridge University Press, 2025. URL: https://doi.org/10.1017/9781009625715.
  36. Damien Pous. Kleene Algebra with Tests and Coq tools for while programs. In Proc. ITP, volume 7998 of LNCS, pages 180-196. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39634-2_15.
  37. Bhakti Shah, Willam Spencer, Laura Zielinski, Ben Caldwell, Adrian Lehmann, and Robert Rand. ViCAR: Visualizing categories with automated rewriting in Coq. Electronic Proceedings in Theoretical Computer Science, 429:234-248, September 2025. URL: https://doi.org/10.4204/eptcs.429.13.
  38. Matthieu Sozeau. A new look at generalized rewriting in type theory. Journal of Formalized Reasoning, 2(1):41-62, 2009. URL: https://doi.org/10.6092/ISSN.1972-5787/1574.
  39. Matthieu Sozeau and Nicolas Oury. First-class type classes. In Proc. TPHOL, LNCS, pages 278-293. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-71067-7_23.
  40. Ross Street. Handbook of algebra. In Categorical structures. Elsevier, 1996. Google Scholar
  41. Enrico Tassi. Elpi: rule-based meta-language for Rocq. In Proc. CoqPL, Denver, United States, January 2025. URL: https://inria.hal.science/hal-04990628.
  42. Djordje Čubrić, Peter Dybjer, and Philip Scott. Normalization and the Yoneda embedding. Mathematical Structures in Computer Science, pages 153-192, 1998. URL: https://doi.org/10.1017/S0960129597002508.
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