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.

Bicategories in univalent foundations / Ahrens, Benedikt; Frumin, Dan; Maggesi, Marco; Veltri, Niccolò; van der Weide, Niels. - In: MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE. - ISSN 0960-1295. - ELETTRONICO. - (2022), pp. 1-38. [10.1017/S0960129522000032]

Bicategories in univalent foundations

Ahrens, Benedikt;Maggesi, Marco;
2022

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.
2022
1
38
Ahrens, Benedikt; Frumin, Dan; Maggesi, Marco; Veltri, Niccolò; van der Weide, Niels
File in questo prodotto:
File Dimensione Formato  
bicategories-in-univalent-foundations.pdf

accesso aperto

Descrizione: Pdf presente sul sito web (versione FirstView, non ha il numero di Issue)
Tipologia: Pdf editoriale (Version of record)
Licenza: Open Access
Dimensione 701.95 kB
Formato Adobe PDF
701.95 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/1260414
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 6
  • ???jsp.display-item.citation.isi??? 3
social impact