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.
2019
4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)
FSCD 2019 International Conference on Formal Structures for Computation and Deduction
Dortmund, Germany
June 24-30,2019
Benedikt Ahrens, Dan Frumin, Marco maggesi, Niels van der Weide
File in questo prodotto:
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.

Utilizza questo identificatore per citare o creare un link a questa risorsa: https://hdl.handle.net/2158/1158732
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 6
  • ???jsp.display-item.citation.isi??? ND
social impact