Bicategories in Univalent Foundations

TL;DR

This paper develops the theory of bicategories within univalent foundations, introducing univalent bicategories and displayed bicategories, with formalization in Coq, expanding the framework of univalent mathematics.

Contribution

It defines and studies univalent bicategories, introduces displayed bicategories for modular construction, and proves key equivalences, all formalized in Coq.

Findings

Several bicategories of interest are univalent.

Every bicategory with univalent hom-categories is weakly equivalent to a univalent bicategory.

The framework is formalized in Coq within the UniMath library.

Abstract

We develop bicategory theory in univalent foundations. Guided by the notion of univalence for (1-)categories studied by Ahrens, Kapulkin, and Shulman, we define and study univalent bicategories. To construct examples of univalent bicategories in a modular fashion, we develop displayed bicategories, an analog of displayed 1-categories introduced by Ahrens and Lumsdaine. We demonstrate the applicability of this notion, and prove that several bicategories of interest are univalent. Among these are the bicategory of univalent categories with families and the bicategory of pseudofunctors between univalent bicategories. Furthermore, we show that every bicategory with univalent hom-categories is weakly equivalent to a univalent bicategory. All of our work is formalized in Coq as part of the UniMath library of univalent mathematics.