License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TYPES.2022.15
URN: urn:nbn:de:0030-drops-184580
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/18458/
Go to the corresponding LIPIcs Volume Portal

Wullaert, Kobe ; Matthes, Ralph ; Ahrens, Benedikt

Univalent Monoidal Categories

pdf-format:
LIPIcs-TYPES-2022-15.pdf (0.9 MB)

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.

BibTeX - Entry

@InProceedings{wullaert_et_al:LIPIcs.TYPES.2022.15,
  author =	{Wullaert, Kobe and Matthes, Ralph and Ahrens, Benedikt},
  title =	{{Univalent Monoidal Categories}},
  booktitle =	{28th International Conference on Types for Proofs and Programs (TYPES 2022)},
  pages =	{15:1--15:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-285-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{269},
  editor =	{Kesner, Delia and P\'{e}drot, Pierre-Marie},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2023/18458},
  URN =		{urn:nbn:de:0030-drops-184580},
  doi =		{10.4230/LIPIcs.TYPES.2022.15},
  annote =	{Keywords: Univalence, Monoidal categories, Rezk completion, Displayed (bi)categories, Proof assistant Coq, UniMath library}
}

Keywords: Univalence, Monoidal categories, Rezk completion, Displayed (bi)categories, Proof assistant Coq, UniMath library
Collection: 28th International Conference on Types for Proofs and Programs (TYPES 2022)
Issue Date: 2023
Date of publication: 28.07.2023

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI