论文标题
单相单体类别
Univalent Monoidal Categories
论文作者
论文摘要
单价类别构成了一个良好的基础中的良好且有用的类别概念。随后，（更高）类别理论中的生物学和其他结构概括了统一的概念。在这里，我们放大了单体类别，并以单价环境进行研究。具体而言，我们表明单相单体类别的生物是无数的。此外，我们为单体类别构建了一个REZK完成：我们展示了任何单体类别如何弱等同于普遍的单相单体类别。我们已经在COQ证明助理中的单个数学库Unimath中完全正式化了这些结果。
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.
