- Publication . Article . Preprint . Conference object . 2022Open Access EnglishAuthors:Benedikt Ahrens; Dan Frumin; Marco Maggesi; Niccolò Veltri; Niels van der Weide;Benedikt Ahrens; Dan Frumin; Marco Maggesi; Niccolò Veltri; Niels van der Weide;Countries: Italy, Netherlands
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. Comment: v1: 16 pages; v2: Veltri added as coauthor, extended version, 32 pages, list of changes given in Section "Publication history"; v3: final journal version to be published in Mathematical Structures in Computer Science; v4: fixed some typos that remain in the MSCS version
Average popularityAverage popularity In bottom 99%Average influencePopularity: Citation-based measure reflecting the current impact.Average influence In bottom 99%Influence: Citation-based measure reflecting the total impact.add Add to ORCIDPlease grant OpenAIRE to access and update your ORCID works.This Research product is the result of merged Research products in OpenAIRE.
You have already added works in your ORCID record related to the merged Research product.
1 Research products, page 1 of 1
Loading
- Publication . Article . Preprint . Conference object . 2022Open Access EnglishAuthors:Benedikt Ahrens; Dan Frumin; Marco Maggesi; Niccolò Veltri; Niels van der Weide;Benedikt Ahrens; Dan Frumin; Marco Maggesi; Niccolò Veltri; Niels van der Weide;Countries: Italy, Netherlands
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. Comment: v1: 16 pages; v2: Veltri added as coauthor, extended version, 32 pages, list of changes given in Section "Publication history"; v3: final journal version to be published in Mathematical Structures in Computer Science; v4: fixed some typos that remain in the MSCS version
Average popularityAverage popularity In bottom 99%Average influencePopularity: Citation-based measure reflecting the current impact.Average influence In bottom 99%Influence: Citation-based measure reflecting the total impact.add Add to ORCIDPlease grant OpenAIRE to access and update your ORCID works.This Research product is the result of merged Research products in OpenAIRE.
You have already added works in your ORCID record related to the merged Research product.