LIPIcs.TYPES.2022.15.pdf
- Filesize: 0.93 MB
- 21 pages
Document
Univalent Monoidal Categories
Authors
Kobe Wullaert 
,
Ralph Matthes ,
Benedikt Ahrens
-
Part of:
Volume:
28th International Conference on Types for Proofs and Programs (TYPES 2022)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Types for Proofs and Programs (TYPES) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2023-07-28
File
Document Identifiers
Author Details
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. Furthermore, we thank Niels van der Weide for helpful discussions on the subject matter and for reviewing the formalization. We also thank Vikraman Choudhury for a question regarding the connection of the monoidal Rezk completion to the Day convolution product. Furthermore, we thank the anonymous referees for their helpful feedback; besides triggering further thoughts on the technical aspects, it helped us to improve the presentation.
Cite As Get BibTex
Kobe Wullaert, Ralph Matthes, and Benedikt Ahrens. Univalent Monoidal Categories. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 15:1-15:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.TYPES.2022.15
Abstract
Univalent categories constitute a well-behaved and useful notion of category in univalent foundations. The notion of univalence has subsequently been generalized to bicategories and other structures in (higher) category theory. Here, we zoom in on monoidal categories and study them in a univalent setting. Specifically, we show that the bicategory of univalent monoidal categories is univalent. Furthermore, we construct a Rezk completion for monoidal categories: we show how any monoidal category is weakly equivalent to a univalent monoidal category, universally. We have fully formalized these results in UniMath, a library of univalent mathematics in the Coq proof assistant.
Subject Classification
ACM Subject Classification
- Theory of computation → Type theory
- Theory of computation → Logic and verification
Keywords
- Univalence
- Monoidal categories
- Rezk completion
- Displayed (bi)categories
- Proof assistant Coq
- UniMath library
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- 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.
- Benedikt Ahrens, Krzysztof Kapulkin, and Michael Shulman. Univalent categories and the Rezk completion. Math. Struct. Comput. Sci., 25(5):1010-1039, 2015. URL: https://doi.org/10.1017/S0960129514000486.
- Benedikt Ahrens and Peter LeFanu Lumsdaine. Displayed categories. Log. Methods Comput. Sci., 15(1), 2019. URL: https://doi.org/10.23638/LMCS-15(1:20)2019.
- Benedikt Ahrens, Paige Randall North, Michael Shulman, and Dimitris Tsementzis. The Univalence Principle, 2021. To be published in Memoirs of the American Mathematical Society. URL: https://arxiv.org/abs/2102.06275.
- Johannes Schipp von Branitz and Ulrik Buchholtz. Using displayed univalent graphs to formalize higher groups in univalent foundations, 2021. URL: https://ulrikbuchholtz.dk/durgs.pdf.
- Lucas Dixon and Aleks Kissinger. Monoidal categories, graphical reasoning, and quantum computation, 2009. Presented at Workshop on Computer Algebra Methods and Commutativity of Algebraic Diagrams (CAM-CAD). URL: https://www.researchgate.net/publication/265098183_Monoidal_Categories_Graphical_Reasoning_and_Quantum_Computation.
- Pau Enrique Moliner, Chris Heunen, and Sean Tull. Space in monoidal categories. Electronic Proceedings in Theoretical Computer Science, 266, April 2017. URL: https://doi.org/10.4204/EPTCS.266.25.
- Geun Bin Im and G.M. Kelly. A universal property of the convolution monoidal structure. Journal of Pure and Applied Algebra, 43(1):75-88, 1986. URL: https://doi.org/10.1016/0022-4049(86)90005-8.
- 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://ems.press/journals/jems/articles/274693.
- Yuri I. Manin and Matilde Marcolli. Homotopy theoretic and categorical models of neural information networks, 2020. URL: https://arxiv.org/abs/2006.15136.
- Chad Nester. Concurrent process histories and resource transducers, 2020. URL: https://arxiv.org/abs/2010.08233.
- Dario Stein and Sam Staton. Compositional semantics for probabilistic programs with exact conditioning. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021, pages 1-13. IEEE, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470552.
- Kirk Sturtz. Categorical probability theory, 2014. URL: https://arxiv.org/abs/1406.6030.
- The Coq Development Team. The Coq proof assistant, version 8.13.0, January 2021. URL: https://zenodo.org/record/4501022.
- The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. http://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
- Niels van der Weide. Constructing Higher Inductive Types. PhD thesis, Radboud University, 2020. URL: https://hdl.handle.net/2066/226923.
- Vladimir Voevodsky, Benedikt Ahrens, Daniel Grayson, et al. UniMath - A computer-checked library of univalent mathematics. Available at http://unimath.github.io/UniMath/ , 2023.