2026-07-22T16:00:30Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:10512 2024-03-06T10:46:06Z ddc:004 open_access

Bicategories in Univalent Foundations Ahrens, Benedikt Frumin, Dan Maggesi, Marco van der Weide, Niels bicategory theory univalent mathematics dependent type theory Coq 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Benedikt Ahrens and Dan Frumin and Marco Maggesi and Niels van der Weide 2019 Is Part Of LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2019.5 urn:nbn:de:0030-drops-105124 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.5 eng https://creativecommons.org/licenses/by/3.0/legalcode