Bicategories in univalent foundations

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

doi:10.4230/LIPIcs.FSCD.2019.5

Bicategories in univalent foundations

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

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

2 Citations (Scopus)

76 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 language	English
Title of host publication	4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)
Editors	Herman Geuvers
Publisher	Schloss Dagstuhl
Pages	5:1-5:17
Number of pages	17
ISBN (Electronic)	9783959771078
DOIs	https://doi.org/10.4230/LIPIcs.FSCD.2019.5
Publication status	Published - 1 Jun 2019
Event	International Conference on Formal Structures for Computation and Deduction (FSCD 2019) - Dortmund, Germany Duration: 24 Jun 2019 → 30 Jun 2019

Publication series

Name	Leibniz International Proceedings in Informatics, LIPIcs
Volume	131
ISSN (Print)	1868-8969

Conference

Conference	International Conference on Formal Structures for Computation and Deduction (FSCD 2019)
Country/Territory	Germany
City	Dortmund
Period	24/06/19 → 30/06/19

Keywords

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

ASJC Scopus subject areas

Software

Access to Document

10.4230/LIPIcs.FSCD.2019.5Licence: Creative Commons: Attribution (CC BY)

Benedikt_Ahrens_et_al_Bicategories_in_univalent_foundations_FSCD_2019
Checked for eligibility: 23/07/2019
Final published version, 575 KBLicence: Creative Commons: Attribution (CC BY)

Cite this

Ahrens, B., Frumin, D., Maggesi, M., & van der Weide, N. (2019). Bicategories in univalent foundations. In H. Geuvers (Ed.), 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019) (pp. 5:1-5:17). Article 5 (Leibniz International Proceedings in Informatics, LIPIcs; Vol. 131). Schloss Dagstuhl. https://doi.org/10.4230/LIPIcs.FSCD.2019.5

@inproceedings{2d6d75565393499ab92bcbd80efaae6d,

title = "Bicategories in univalent foundations",

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 {\textquoteleft}displayed bicategories{\textquoteright}, 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.",

keywords = "bicategory theory, univalent mathematics, dependent type theory, Coq, Dependent type theory, Bicategory theory, Univalent mathematics",

author = "Benedikt Ahrens and Dan Frumin and Marco Maggesi and {van der Weide}, Niels",

year = "2019",

month = jun,

day = "1",

doi = "10.4230/LIPIcs.FSCD.2019.5",

language = "English",

series = "Leibniz International Proceedings in Informatics, LIPIcs",

publisher = "Schloss Dagstuhl",

pages = "5:1--5:17",

editor = "Herman Geuvers",

booktitle = "4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)",

address = "Germany",

note = "International Conference on Formal Structures for Computation and Deduction (FSCD 2019) ; Conference date: 24-06-2019 Through 30-06-2019",

}

Ahrens, B, Frumin, D, Maggesi, M & van der Weide, N 2019, Bicategories in univalent foundations. in H Geuvers (ed.), 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)., 5, Leibniz International Proceedings in Informatics, LIPIcs, vol. 131, Schloss Dagstuhl, pp. 5:1-5:17, International Conference on Formal Structures for Computation and Deduction (FSCD 2019), Dortmund, Germany, 24/06/19. https://doi.org/10.4230/LIPIcs.FSCD.2019.5

Bicategories in univalent foundations. / Ahrens, Benedikt; Frumin, Dan; Maggesi, Marco et al.
4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). ed. / Herman Geuvers. Schloss Dagstuhl, 2019. p. 5:1-5:17 5 (Leibniz International Proceedings in Informatics, LIPIcs; Vol. 131).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Bicategories in univalent foundations

AU - Ahrens, Benedikt

AU - Frumin, Dan

AU - Maggesi, Marco

AU - van der Weide, Niels

PY - 2019/6/1

Y1 - 2019/6/1

N2 - 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.

AB - 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.

KW - bicategory theory

KW - univalent mathematics

KW - dependent type theory

KW - Coq

KW - Dependent type theory

KW - Bicategory theory

KW - Univalent mathematics

UR - http://www.scopus.com/inward/record.url?scp=85068065003&partnerID=8YFLogxK

U2 - 10.4230/LIPIcs.FSCD.2019.5

DO - 10.4230/LIPIcs.FSCD.2019.5

M3 - Conference contribution

T3 - Leibniz International Proceedings in Informatics, LIPIcs

SP - 5:1-5:17

BT - 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)

A2 - Geuvers, Herman

PB - Schloss Dagstuhl

T2 - International Conference on Formal Structures for Computation and Deduction (FSCD 2019)

Y2 - 24 June 2019 through 30 June 2019

ER -