文章基本信息

标题：Bicategories in Univalent Foundations
本地全文：下载
作者：Benedikt Ahrens ; Dan Frumin ; Marco Maggesi 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2019
卷号：131
页码：1-17
DOI：10.4230/LIPIcs.FSCD.2019.5
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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.
关键词：bicategory theory; univalent mathematics; dependent type theory; Coq