Creative Commons Attribution 3.0 Unported license (CC-BY 3.0)when quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2019.5
URN: urn:nbn:de:0030-drops-105124
URL: https://drops.dagstuhl.de/opus/volltexte/2019/10512/
Ahrens, Benedikt ; Frumin, Dan ; Maggesi, Marco ; van der Weide, Niels
Bicategories in Univalent Foundations
| pdf-format: |
|
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.
BibTeX - Entry
@InProceedings{ahrens_et_al:LIPIcs:2019:10512,
author = {Benedikt Ahrens and Dan Frumin and Marco Maggesi and Niels van der Weide},
title = {{Bicategories in Univalent Foundations}},
booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
pages = {5:1--5:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-107-8},
ISSN = {1868-8969},
year = {2019},
volume = {131},
editor = {Herman Geuvers},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2019/10512},
URN = {urn:nbn:de:0030-drops-105124},
doi = {10.4230/LIPIcs.FSCD.2019.5},
annote = {Keywords: bicategory theory, univalent mathematics, dependent type theory, Coq}
}
| Keywords: | bicategory theory, univalent mathematics, dependent type theory, Coq | |
| Seminar: | 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019) | |
| Issue date: | 2019 | |
| Date of publication: | 18.06.2019 |
