Bicategories in univalent foundations

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

Authors

Colleges, School and Institutes

External organisations

  • Radboud University, Nijmegen, The Netherlands
  • Università degli Studi di Firenze, Italy

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.

Details

Original languageEnglish
Title of host publication4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)
EditorsHerman Geuvers
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)
CountryGermany
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