Univalent Monoidal Categories

TL;DR

This paper explores univalent monoidal categories within univalent foundations, demonstrating their properties, constructing a Rezk completion, and formalizing results in UniMath using Coq.

Contribution

It establishes the univalence of the bicategory of monoidal categories and constructs a universal Rezk completion for monoidal categories.

Findings

The bicategory of univalent monoidal categories is univalent.

Every monoidal category has a weakly equivalent univalent version.

Results are fully formalized in UniMath using Coq.

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.