Univalent Monoidal Categories
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.
Keywords
Cite
@article{arxiv.2212.03146,
title = {Univalent Monoidal Categories},
author = {Kobe Wullaert and Ralph Matthes and Benedikt Ahrens},
journal= {arXiv preprint arXiv:2212.03146},
year = {2023}
}
Comments
21 pages, accepted for the TYPES'22 postproceedings volume in the LIPIcs series by Schlo{\ss} Dagstuhl (editors: Delia Kesner and Pierre-Marie P\'edrot)