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 those, we develop the notion of “displayed bicategories”, an analog of displayed 1-categories introduced by Ahrens and Lumsdaine. Displayed bicategories allow us to construct univalent bicategories in a modular fashion. To demonstrate the applicability of this notion, we prove several bicategories are univalent. Among these are the bicategory of univalent categories with families and the bicategory of pseudofunctors between univalent bicategories. Our work is formalized in the UniMath library of univalent mathematics.
Bicategories in Univalent Foundations / Benedikt Ahrens, Dan Frumin, Marco maggesi, Niels van der Weide. - ELETTRONICO. - 5:(2019), pp. 1-17. (Intervento presentato al convegno FSCD 2019 International Conference on Formal Structures for Computation and Deduction tenutosi a Dortmund, Germany nel June 24-30,2019) [10.4230/LIPIcs.FSCD.2019.5].
Bicategories in Univalent Foundations
Benedikt Ahrens;Marco maggesi;
2019
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 those, we develop the notion of “displayed bicategories”, an analog of displayed 1-categories introduced by Ahrens and Lumsdaine. Displayed bicategories allow us to construct univalent bicategories in a modular fashion. To demonstrate the applicability of this notion, we prove several bicategories are univalent. Among these are the bicategory of univalent categories with families and the bicategory of pseudofunctors between univalent bicategories. Our work is formalized in the UniMath library of univalent mathematics.File | Dimensione | Formato | |
---|---|---|---|
LIPIcs-FSCD-2019-5.pdf
accesso aperto
Descrizione: Versione pubblicata online dall'editore
Tipologia:
Pdf editoriale (Version of record)
Licenza:
Creative commons
Dimensione
574.76 kB
Formato
Adobe PDF
|
574.76 kB | Adobe PDF | |
1903.01152v1.pdf
accesso aperto
Descrizione: Versione ArXiv v1 2020-03-04
Tipologia:
Versione finale referata (Postprint, Accepted manuscript)
Licenza:
Open Access
Dimensione
609.28 kB
Formato
Adobe PDF
|
609.28 kB | Adobe PDF |
I documenti in FLORE sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.