Bicategories in univalent foundations

Benedikt Ahrens, Dan Frumin, Marco Maggesi, Niels van der Weide

Research output: Chapter in Book/Report/Conference proceedingConference contribution

2 Citations (Scopus)
41 Downloads (Pure)

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.
Original languageEnglish
Title of host publication4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)
EditorsHerman Geuvers
PublisherSchloss Dagstuhl
Pages5:1-5:17
Number of pages17
ISBN (Electronic)9783959771078
DOIs
Publication statusPublished - 1 Jun 2019
EventInternational Conference on Formal Structures for Computation and Deduction (FSCD 2019) - Dortmund, Germany
Duration: 24 Jun 201930 Jun 2019

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume131
ISSN (Print)1868-8969

Conference

ConferenceInternational Conference on Formal Structures for Computation and Deduction (FSCD 2019)
Country/TerritoryGermany
CityDortmund
Period24/06/1930/06/19

Keywords

  • bicategory theory
  • univalent mathematics
  • dependent type theory
  • Coq
  • Dependent type theory
  • Bicategory theory
  • Univalent mathematics

ASJC Scopus subject areas

  • Software

Cite this