Bicategories in univalent foundations

Journal article (2022)

Authors

B.P. Ahrens University of Birmingham, Programming Languages - EEMCS
Dan Frumin Rijksuniversiteit Groningen
Marco Maggesi University of Florence
Niccolò Veltri Tallinn University of Technology
Niels Van Der Weide Radboud Universiteit Nijmegen, University of Birmingham
Research Group
Programming Languages (EEMCS) (TU Delft)
Copyright: © 2022 B.P. Ahrens, Dan Frumin, Marco Maggesi, Niccolò Veltri, Niels van der Weide
DOI: https://doi.org/10.1017/S0960129522000032
More Info
expand_more

Published Date

2022

Language

English

Faculty

Electrical Engineering, Mathematics and Computer Science

Department

Software Technology

Research Group

Programming Languages

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.