Bicategories in univalent foundations

Benedikt Ahrens; Dan Frumin; Marco  Maggesi; Niccolò Veltri; Niels  Van Der Weide

doi:10.1017/S0960129522000032

Bicategories in univalent foundations

Benedikt Ahrens, Dan Frumin, Marco Maggesi, Niccolò Veltri, Niels Van Der Weide

Computer Science

Research output: Contribution to journal › Article › peer-review

52 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 univalent bicategories in a modular fashion, we develop displayed bicategories, an analog of displayed 1-categories introduced by Ahrens and Lumsdaine. We demonstrate the applicability of this notion and prove that several bicategories of interest are univalent. Among these are the bicategory of univalent categories with families and the bicategory of pseudofunctors between univalent bicategories. Furthermore, we show that every bicategory with univalent hom-categories is weakly equivalent to a univalent bicategory. All of our work is formalized in Coq as part of the UniMath library of univalent mathematics.

Original language	English
Journal	Mathematical Structures in Computer Science
Early online date	9 Mar 2022
DOIs	https://doi.org/10.1017/S0960129522000032
Publication status	E-pub ahead of print - 9 Mar 2022

Bibliographical note

Funding Information:
We thank Peter LeFanu Lumsdaine and Michael Shulman for helpful discussions on the subject matter, and James Leslie for pointing out several typos in the conference version of this article. We furthermore thank the referees for their careful reading and thoughtful and constructive criticism. Work on this article was supported by a grant from the COST Action EUTypes CA15123. We would like to express our gratitude to all the EUTypes actors for their support. This work was partially funded by EPSRC under agreement number EP/T000252/1. This material is based upon work supported by the Air Force Office of Scientific Research under award number FA9550-17-1-0363. Ahrens acknowledges the support of the Centre for Advanced Study (CAS) in Oslo, Norway, which funded and hosted the research project Homotopy Type Theory and Univalent Foundations during the 2018/19 academic year. Frumin was supported by the Netherlands Organisation for Scientific Research (NWO/TTW) under the STW project 14319 and VIDI Project No. 016.Vidi.189.046. Maggesi was supported by MIUR and GNSAGA-INdAM. Veltri was supported by the Estonian Research Council grant PSG659 and by the ESF funded Estonian IT Academy research measure (project 2014-2020.4.05.19-0001).

Publisher Copyright:
© The Author(s), 2022. Published by Cambridge University Press.

Keywords

Bicategory theory
Coq
dependent type theory
univalent mathematics

ASJC Scopus subject areas

Mathematics (miscellaneous)
Computer Science Applications

Access to Document

10.1017/S0960129522000032Licence: Creative Commons: Attribution (CC BY)

AhrensB2022BicategoriesFinal published version, 697 KBLicence: Creative Commons: Attribution (CC BY)

Cite this

@article{ff9dcc66da324a7cbf56b2c8e868334b,

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 univalent bicategories in a modular fashion, we develop displayed bicategories, an analog of displayed 1-categories introduced by Ahrens and Lumsdaine. We demonstrate the applicability of this notion and prove that several bicategories of interest are univalent. Among these are the bicategory of univalent categories with families and the bicategory of pseudofunctors between univalent bicategories. Furthermore, we show that every bicategory with univalent hom-categories is weakly equivalent to a univalent bicategory. All of our work is formalized in Coq as part of the UniMath library of univalent mathematics.",

keywords = "Bicategory theory, Coq, dependent type theory, univalent mathematics",

author = "Benedikt Ahrens and Dan Frumin and Marco Maggesi and Niccol{\`o} Veltri and {Van Der Weide}, Niels",

note = "Funding Information: We thank Peter LeFanu Lumsdaine and Michael Shulman for helpful discussions on the subject matter, and James Leslie for pointing out several typos in the conference version of this article. We furthermore thank the referees for their careful reading and thoughtful and constructive criticism. Work on this article was supported by a grant from the COST Action EUTypes CA15123. We would like to express our gratitude to all the EUTypes actors for their support. This work was partially funded by EPSRC under agreement number EP/T000252/1. This material is based upon work supported by the Air Force Office of Scientific Research under award number FA9550-17-1-0363. Ahrens acknowledges the support of the Centre for Advanced Study (CAS) in Oslo, Norway, which funded and hosted the research project Homotopy Type Theory and Univalent Foundations during the 2018/19 academic year. Frumin was supported by the Netherlands Organisation for Scientific Research (NWO/TTW) under the STW project 14319 and VIDI Project No. 016.Vidi.189.046. Maggesi was supported by MIUR and GNSAGA-INdAM. Veltri was supported by the Estonian Research Council grant PSG659 and by the ESF funded Estonian IT Academy research measure (project 2014-2020.4.05.19-0001). Publisher Copyright: {\textcopyright} The Author(s), 2022. Published by Cambridge University Press.",

year = "2022",

month = mar,

day = "9",

doi = "10.1017/S0960129522000032",

language = "English",

journal = "Mathematical Structures in Computer Science",

issn = "0960-1295",

publisher = "Cambridge University Press",

}

TY - JOUR

T1 - Bicategories in univalent foundations

AU - Ahrens, Benedikt

AU - Frumin, Dan

AU - Maggesi, Marco

AU - Veltri, Niccolò

AU - Van Der Weide, Niels

N1 - Funding Information: We thank Peter LeFanu Lumsdaine and Michael Shulman for helpful discussions on the subject matter, and James Leslie for pointing out several typos in the conference version of this article. We furthermore thank the referees for their careful reading and thoughtful and constructive criticism. Work on this article was supported by a grant from the COST Action EUTypes CA15123. We would like to express our gratitude to all the EUTypes actors for their support. This work was partially funded by EPSRC under agreement number EP/T000252/1. This material is based upon work supported by the Air Force Office of Scientific Research under award number FA9550-17-1-0363. Ahrens acknowledges the support of the Centre for Advanced Study (CAS) in Oslo, Norway, which funded and hosted the research project Homotopy Type Theory and Univalent Foundations during the 2018/19 academic year. Frumin was supported by the Netherlands Organisation for Scientific Research (NWO/TTW) under the STW project 14319 and VIDI Project No. 016.Vidi.189.046. Maggesi was supported by MIUR and GNSAGA-INdAM. Veltri was supported by the Estonian Research Council grant PSG659 and by the ESF funded Estonian IT Academy research measure (project 2014-2020.4.05.19-0001). Publisher Copyright: © The Author(s), 2022. Published by Cambridge University Press.

PY - 2022/3/9

Y1 - 2022/3/9

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 univalent bicategories in a modular fashion, we develop displayed bicategories, an analog of displayed 1-categories introduced by Ahrens and Lumsdaine. We demonstrate the applicability of this notion and prove that several bicategories of interest are univalent. Among these are the bicategory of univalent categories with families and the bicategory of pseudofunctors between univalent bicategories. Furthermore, we show that every bicategory with univalent hom-categories is weakly equivalent to a univalent bicategory. All of our work is formalized in Coq as part of 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 univalent bicategories in a modular fashion, we develop displayed bicategories, an analog of displayed 1-categories introduced by Ahrens and Lumsdaine. We demonstrate the applicability of this notion and prove that several bicategories of interest are univalent. Among these are the bicategory of univalent categories with families and the bicategory of pseudofunctors between univalent bicategories. Furthermore, we show that every bicategory with univalent hom-categories is weakly equivalent to a univalent bicategory. All of our work is formalized in Coq as part of the UniMath library of univalent mathematics.

KW - Bicategory theory

KW - Coq

KW - dependent type theory

KW - univalent mathematics

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

U2 - 10.1017/S0960129522000032

DO - 10.1017/S0960129522000032

M3 - Article

SN - 0960-1295

JO - Mathematical Structures in Computer Science

JF - Mathematical Structures in Computer Science

ER -

Bicategories in univalent foundations

Abstract

Bibliographical note

Keywords

ASJC Scopus subject areas

Access to Document

Fingerprint

Cite this