Bicategories in Univalent Foundations

Authors

Benedikt Ahrens, Dan Frumin, Marco Maggesi, Niccolò Veltri, Niels van der Weide

Type: Preprint

Publication Date: 2019-03-04

Citations: 0

View Ask PDF

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, 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. 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-category is weakly equivalent to a univalent bicategory. All of our work is formalized in Coq as part of the UniMath library of univalent mathematics.

Locations

arXiv (Cornell University)
View

Ask a Question About This Paper

Summary

Similar Works

Bicategories in univalent foundations

2021-11-01

Benedikt Ahrens , Dan Frumin , Marco Maggesi +2 more

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

Chat View PDF

Bicategories in Univalent Foundations

2019-06-01

Benedikt Ahrens , Dan Frumin , Marco Maggesi +1 more

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

Univalent Monoidal Categories

2022-01-01

Kobe Wullaert , Ralph Matthes , Benedikt Ahrens

Univalent categories constitute a well-behaved and useful notion of category in univalent foundations. The notion of univalence has subsequently been generalized to bicategories and other structures in (higher) category theory. … Univalent categories constitute a well-behaved and useful notion of category in univalent foundations. The notion of univalence has subsequently been generalized to bicategories and other structures in (higher) category theory. Here, we zoom in on monoidal categories and study them in a univalent setting. Specifically, we show that the bicategory of univalent monoidal categories is univalent. Furthermore, we construct a Rezk completion for monoidal categories: we show how any monoidal category is weakly equivalent to a univalent monoidal category, universally. We have fully formalized these results in UniMath, a library of univalent mathematics in the Coq proof assistant.

Chat View PDF

Univalent Monoidal Categories

2023-07-28

Kobe Wullaert , Ralph Matthes , Benedikt Ahrens

Chat View PDF

Insights From Univalent Foundations: A Case Study Using Double Categories

2024-02-07

Nima Rasekh , Niels van der Weide , Benedikt Ahrens +1 more

Category theory unifies mathematical concepts, aiding comparisons across structures by incorporating objects and morphisms, which capture their interactions. It has influenced areas of computer science such as automata theory, functional … Category theory unifies mathematical concepts, aiding comparisons across structures by incorporating objects and morphisms, which capture their interactions. It has influenced areas of computer science such as automata theory, functional programming, and semantics. Certain objects naturally exhibit two classes of morphisms, leading to the concept of a double category, which has found applications in computing science (e.g., ornaments, profunctor optics, denotational semantics). The emergence of diverse categorical structures motivated a unified framework for category theory. However, unlike other mathematical objects, classification of categorical structures faces challenges due to various relevant equivalences. This poses significant challenges when pursuing the formalization of categories and restricts the applicability of powerful techniques, such as transport along equivalences. This work contends that univalent foundations offers a suitable framework for classifying different categorical structures based on desired notions of equivalences, and remedy the challenges when formalizing categories. The richer notion of equality in univalent foundations makes the equivalence of a categorical structure an inherent part of its structure. We concretely apply this analysis to double categorical structures. We characterize and formalize various definitions in Coq UniMath, including (pseudo) double categories and double bicategories, up to chosen equivalences. We also establish univalence principles, making chosen equivalences part of the double categorical structure, analyzing strict double setcategories (invariant under isomorphisms), pseudo double setcategories (invariant under isomorphisms), univalent pseudo double categories (invariant under vertical equivalences) and univalent double bicategories (invariant under gregarious equivalences).

Chat View PDF

Univalent Double Categories

2024-01-09

Niels van der Weide , Nima Rasekh , Benedikt Ahrens +1 more

Chat View PDF

The Formal Theory of Monads, Univalently

2025-02-19

Niels van der Weide

We develop the formal theory of monads, as established by Street, in univalent foundations. This allows us to formally reason about various kinds of monads on the right level of … We develop the formal theory of monads, as established by Street, in univalent foundations. This allows us to formally reason about various kinds of monads on the right level of abstraction. In particular, we define the bicategory of monads internal to a bicategory, and prove that it is univalent. We also define Eilenberg-Moore objects, and we show that both Eilenberg-Moore categories and Kleisli categories give rise to Eilenberg-Moore objects. Finally, we relate monads and adjunctions in arbitrary bicategories. Our work is formalized in Coq using the UniMath library.

Chat View PDF

The Formal Theory of Monads, Univalently

2022-01-01

Niels van der Weide

Chat View PDF

Univalent Double Categories

2023-01-01

Niels van der Weide , Nima Rasekh , Benedikt Ahrens +1 more

Category theory is a branch of mathematics that provides a formal framework for understanding the relationship between mathematical structures. To this end, a category not only incorporates the data of … Category theory is a branch of mathematics that provides a formal framework for understanding the relationship between mathematical structures. To this end, a category not only incorporates the data of the desired objects, but also "morphisms", which capture how different objects interact with each other. Category theory has found many applications in mathematics and in computer science, for example in functional programming. Double categories are a natural generalization of categories which incorporate the data of two separate classes of morphisms, allowing a more nuanced representation of relationships and interactions between objects. Similar to category theory, double categories have been successfully applied to various situations in mathematics and computer science, in which objects naturally exhibit two types of morphisms. Examples include categories themselves, but also lenses, petri nets, and spans. While categories have already been formalized in a variety of proof assistants, double categories have received far less attention. In this paper we remedy this situation by presenting a formalization of double categories via the proof assistant Coq, relying on the Coq UniMath library. As part of this work we present two equivalent formalizations of the definition of a double category, an unfolded explicit definition and a second definition which exhibits excellent formal properties via 2-sided displayed categories. As an application of the formal approach we establish a notion of univalent double category along with a univalence principle: equivalences of univalent double categories coincide with their identities

Chat View PDF

Categorical structures for type theory in univalent foundations

2017-01-01

Benedikt Ahrens , Peter LeFanu Lumsdaine , Vladimir Voevodsky

In this paper, we analyze and compare three of the many algebraic structures that have been used for modeling dependent type theories: categories with families, split type-categories, and representable maps … In this paper, we analyze and compare three of the many algebraic structures that have been used for modeling dependent type theories: categories with families, split type-categories, and representable maps of presheaves. We study these in univalent type theory, where the comparisons between them can be given more elementarily than in set-theoretic foundations. Specifically, we construct maps between the various types of structures, and show that assuming the Univalence axiom, some of the comparisons are equivalences. We then analyze how these structures transfer along (weak and strong) equivalences of categories, and, in particular, show how they descend from a category (not assumed univalent/saturated) to its Rezk completion. To this end, we introduce relative universes, generalizing the preceding notions, and study the transfer of such relative universes along suitable structure. We work throughout in (intensional) dependent type theory; some results, but not all, assume the univalence axiom. All the material of this paper has been formalized in Coq, over the UniMath library.

Chat View PDF

Univalence in locally cartesian closed ∞-categories

2016-11-06

David Gepner , Joachim Kock

Abstract After developing the basic theory of locally cartesian localizations of presentable locally cartesian closed <m:math xmlns:m="http://www.w3.org/1998/Math/MathML"> <m:mi>∞</m:mi> </m:math> ${\infty}$ -categories, we establish the representability of equivalences and show that … Abstract After developing the basic theory of locally cartesian localizations of presentable locally cartesian closed <m:math xmlns:m="http://www.w3.org/1998/Math/MathML"> <m:mi>∞</m:mi> </m:math> ${\infty}$ -categories, we establish the representability of equivalences and show that univalent families, in the sense of Voevodsky, form a poset isomorphic to the poset of bounded local classes, in the sense of Lurie. It follows that every <m:math xmlns:m="http://www.w3.org/1998/Math/MathML"> <m:mi>∞</m:mi> </m:math> ${\infty}$ -topos has a hierarchy of “universal” univalent families, indexed by regular cardinals, and that n -topoi have univalent families classifying <m:math xmlns:m="http://www.w3.org/1998/Math/MathML"> <m:mrow> <m:mo>(</m:mo> <m:mrow> <m:mi>n</m:mi> <m:mo>-</m:mo> <m:mn>2</m:mn> </m:mrow> <m:mo>)</m:mo> </m:mrow> </m:math> ${(n-2)}$ -truncated maps. We show that univalent families are preserved (and detected) by right adjoints to locally cartesian localizations, and use this to exhibit certain canonical univalent families in <m:math xmlns:m="http://www.w3.org/1998/Math/MathML"> <m:mi>∞</m:mi> </m:math> $\infty$ -quasitopoi (certain <m:math xmlns:m="http://www.w3.org/1998/Math/MathML"> <m:mi>∞</m:mi> </m:math> ${\infty}$ -categories of “separated presheaves”, introduced here). We also exhibit some more exotic examples of univalent families, illustrating that a univalent family in an n -topos need not be <m:math xmlns:m="http://www.w3.org/1998/Math/MathML"> <m:mrow> <m:mo>(</m:mo> <m:mrow> <m:mi>n</m:mi> <m:mo>-</m:mo> <m:mn>2</m:mn> </m:mrow> <m:mo>)</m:mo> </m:mrow> </m:math> ${(n-2)}$ -truncated, as well as some univalent families in the Morel–Voevodsky <m:math xmlns:m="http://www.w3.org/1998/Math/MathML"> <m:mi>∞</m:mi> </m:math> ${\infty}$ -category of motivic spaces, an instance of a locally cartesian closed <m:math xmlns:m="http://www.w3.org/1998/Math/MathML"> <m:mi>∞</m:mi> </m:math> ${\infty}$ -category which is not an n -topos for any <m:math xmlns:m="http://www.w3.org/1998/Math/MathML"> <m:mrow> <m:mn>0</m:mn> <m:mo>≤</m:mo> <m:mi>n</m:mi> <m:mo>≤</m:mo> <m:mi>∞</m:mi> </m:mrow> </m:math> ${0\leq n\leq\infty}$ . Lastly, we show that any presentable locally cartesian closed <m:math xmlns:m="http://www.w3.org/1998/Math/MathML"> <m:mi>∞</m:mi> </m:math> ${\infty}$ -category is modeled by a combinatorial type-theoretic model category, and conversely that the <m:math xmlns:m="http://www.w3.org/1998/Math/MathML"> <m:mi>∞</m:mi> </m:math> ${\infty}$ -category underlying a combinatorial type-theoretic model category is presentable and locally cartesian closed. Under this correspondence, univalent families in presentable locally cartesian closed <m:math xmlns:m="http://www.w3.org/1998/Math/MathML"> <m:mi>∞</m:mi> </m:math> ${\infty}$ -categories correspond to univalent fibrations in combinatorial type-theoretic model categories.

Univalent Higher Categories via Complete Semi-Segal Types

2018-01-07

Paolo Capriotti , Nicolai Kraus

Category theory in homotopy type theory is intricate as categorical laws can only be stated “up to homotopy”, and thus require coherences. The established notion of a univalent category (Ahrens … Category theory in homotopy type theory is intricate as categorical laws can only be stated “up to homotopy”, and thus require coherences. The established notion of a univalent category (Ahrens et al. 2015) solves this by considering only truncated types, and it roughly corresponds to an ordinary category. The drawback is that univalent categories fail to capture many naturally occurring structures, such as type universes or the type of univalent categories themselves. This stems from the fact that the natural notion of a category in homotopy type theory is not that of an ordinary, but rather a higher category.

The internal languages of univalent categories

2024-11-10

Niels van der Weide

Internal language theorems are fundamental in categorical logic, since they express an equivalence between syntax and semantics. One of such theorems was proven by Clairambault and Dybjer, who corrected the … Internal language theorems are fundamental in categorical logic, since they express an equivalence between syntax and semantics. One of such theorems was proven by Clairambault and Dybjer, who corrected the result originally by Seely. More specifically, they constructed a biequivalence between the bicategory of locally Cartesian closed categories and the bicategory of democratic categories with families with extensional identity types, $\sum$-types, and $\prod$-types. This theorem expresses that the internal language of locally Cartesian closed is extensional Martin-L\"of type theory with dependent sums and products. In this paper, we study the theorem by Clairambault and Dybjer for univalent categories, and we extend it to various classes of toposes, among which are $\prod$-pretoposes and elementary toposes. The results in this paper have been formalized using the proof assistant Coq and the UniMath library.

Chat View PDF

fc-multicategories

1999-02-28

Tom Leinster

fc-multicategories are a very general kind of two-dimensional structure, encompassing bicategories, monoidal categories, double categories and ordinary multicategories. We define them and explain how they provide a natural setting for … fc-multicategories are a very general kind of two-dimensional structure, encompassing bicategories, monoidal categories, double categories and ordinary multicategories. We define them and explain how they provide a natural setting for two familiar categorical ideas. The first is the bimodules construction, traditionally carried out on suitably cocomplete bicategories but perhaps more naturally carried out on fc-multicategories. The second is enrichment: there is a theory of categories enriched in an fc-multicategory, extending the usual theory of enrichment in a monoidal category. We finish by indicating how this work is just the simplest case of a much larger phenomenon.

Chat View PDF

fc-multicategories

1999-01-01

Tom Leinster

Chat View PDF

Univalent categories and the Rezk completion

2015-01-19

Benedikt Ahrens , Krzysztof Kapulkin , Michael Shulman

We develop category theory within Univalent Foundations, which is a foundational system for mathematics based on a homotopical interpretation of dependent type theory. In this system, we propose a definition … We develop category theory within Univalent Foundations, which is a foundational system for mathematics based on a homotopical interpretation of dependent type theory. In this system, we propose a definition of ‘category’ for which equality and equivalence of categories agree. Such categories satisfy a version of the univalence axiom, saying that the type of isomorphisms between any two objects is equivalent to the identity type between these objects; we call them ‘saturated’ or ‘univalent’ categories. Moreover, we show that any category is weakly equivalent to a univalent one in a universal way. In homotopical and higher-categorical semantics, this construction corresponds to a truncated version of the Rezk completion for Segal spaces, and also to the stack completion of a prestack.

Chat View PDF

Functional bivarieties in functor categories

1975-01-01

E. G. Shul’geifer

Univalent Categories and the Rezk Completion

2015-01-01

Benedikt Ahrens , Krzysztof Kapulkin , Michael Shulman

Chat View PDF

Univalence in Higher Category Theory

2021-01-01

Nima Rasekh

Univalence was first defined in the setting of homotopy type theory by Voevodsky, who also (along with Kapulkin and Lumsdaine) adapted it to a model categorical setting, which was subsequently … Univalence was first defined in the setting of homotopy type theory by Voevodsky, who also (along with Kapulkin and Lumsdaine) adapted it to a model categorical setting, which was subsequently generalized to locally Cartesian closed presentable $\infty$-categories by Gepner and Kock. These definitions were used to characterize various $\infty$-categories as models of type theories. We give a definition for univalent morphisms in finitely complete $\infty$-categories that generalizes the aforementioned definitions and completely focuses on the $\infty$-categorical aspects, characterizing it via representability of certain functors, which should remind the reader of concepts such as adjunctions or limits. We then prove that in a locally Cartesian closed $\infty$-category (that is not necessarily presentable) univalence of a morphism is equivalent to the completeness of a certain Segal object we construct out of the morphism, characterizing univalence via internal $\infty$-categories, which had been considered in a strict setting by Stenzel. We use these results to study the connection between univalence and elementary topos theory. We also study univalent morphisms in the category of groups, the $\infty$-category of $\infty$-categories, and pointed $\infty$-categories.

Chat View PDF

Introduction to bicategories

1967-01-01

Jean Bénabou

Cited by (0)

References (11)

Discrete Generalised Polynomial Functors

2012-01-01

Marcelo Fiore

Internal type theory

1996-01-01

Peter Dybjer

Introduction to bicategories

1967-01-01

Jean Bénabou

Univalent categories and the Rezk completion

2015-01-19

Benedikt Ahrens , Krzysztof Kapulkin , Michael Shulman

Chat View PDF

The Simplicial Model of Univalent Foundations (after Voevodsky)

2012-11-12

Chris Kapulkin , Peter LeFanu Lumsdaine

We present Voevodsky's construction of a model of univalent type theory in the category of simplicial sets. To this end, we first give a general technique for constructing categorical models … We present Voevodsky's construction of a model of univalent type theory in the category of simplicial sets. To this end, we first give a general technique for constructing categorical models of dependent type theory, using universes to obtain coherence. We then construct a (weakly) universal Kan fibration, and use it to exhibit a model in simplicial sets. Lastly, we introduce the Univalence Axiom, in several equivalent formulations, and show that it holds in our model. As a corollary, we conclude that Martin-Lof type theory with one univalent universe (formulated in terms of contextual categories) is at least as consistent as ZFC with two inaccessible cardinals.

Chat View PDF

Finitary Higher Inductive Types in the Groupoid Model

2018-04-01

Peter Dybjer , Hugo Moeneclaey

A higher inductive type of level 1 (a 1-hit) has constructors for points and paths only, whereas a higher inductive type of level 2 (a 2-hit) has constructors for surfaces … A higher inductive type of level 1 (a 1-hit) has constructors for points and paths only, whereas a higher inductive type of level 2 (a 2-hit) has constructors for surfaces too. We restrict attention to finitary higher inductive types and present general schemata for the types of their point, path, and surface constructors. We also derive the elimination and equality rules from the types of constructors for 1-hits and 2-hits. Moreover, we construct a groupoid model for dependent type theory with 2-hits and point out that we obtain a setoid model for dependent type theory with 1-hits by truncating the groupoid model.

Categorical structures for type theory in univalent foundations

2017-01-01

Benedikt Ahrens , Peter LeFanu Lumsdaine , Vladimir Voevodsky

Chat View PDF

Bicategories in Univalent Foundations

2019-06-01

Benedikt Ahrens , Dan Frumin , Marco Maggesi +1 more

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

Natural models of homotopy type theory

2016-11-17

Steve Awodey

The notion of a natural model of type theory is defined in terms of that of a representable natural transfomation of presheaves. It is shown that such models agree exactly … The notion of a natural model of type theory is defined in terms of that of a representable natural transfomation of presheaves. It is shown that such models agree exactly with the concept of a category with families in the sense of Dybjer, which can be regarded as an algebraic formulation of type theory. We determine conditions for such models to satisfy the inference rules for dependent sums Σ, dependent products Π and intensional identity types Id , as used in homotopy type theory. It is then shown that a category admits such a model if it has a class of maps that behave like the abstract fibrations in axiomatic homotopy theory: They should be stable under pullback, closed under composition and relative products, and there should be weakly orthogonal factorizations into the class. It follows that many familiar settings for homotopy theory also admit natural models of the basic system of homotopy type theory.

Chat View PDF

Univalent higher categories via complete Semi-Segal types

2017-12-27

Paolo Capriotti , Nicolai Kraus

Category theory in homotopy type theory is intricate as categorical laws can only be stated "up to homotopy", and thus require coherences. The established notion of a univalent category (as … Category theory in homotopy type theory is intricate as categorical laws can only be stated "up to homotopy", and thus require coherences. The established notion of a univalent category (as introduced by Ahrens et al.) solves this by considering only truncated types, roughly corresponding to an ordinary category. This fails to capture many naturally occurring structures, stemming from the fact that the naturally occurring structures in homotopy type theory are not ordinary, but rather higher categories. Out of the large variety of approaches to higher category theory that mathematicians have proposed, we believe that, for type theory, the simplicial strategy is best suited. Work by Lurie and Harpaz motivates the following definition. Given the first ( n +3) levels of a semisimplicial type S , we can equip S with three properties: first, contractibility of the types of certain horn fillers; second, a completeness property; and third, a truncation condition. We call this a complete semi-Segal n -type . This is very similar to an earlier suggestion by Schreiber. The definition of a univalent (1-) category by Ahrens et al. can easily be extended or restricted to the definition of a univalent n -category (more precisely, ( n ,1)-category) for n ∈ {0,1,2}, and we show that the type of complete semi-Segal n -types is equivalent to the type of univalent n -categories in these cases. Thus, we believe that the notion of a complete semi-Segal n -type can be taken as the definition of a univalent n -category. We provide a formalisation in the proof assistant Agda using a completely explicit representation of semi-simplicial types for levels up to 4.

Chat View PDF

The biequivalence of locally cartesian closed categories and Martin-Löf type theories

2014-04-29

Pierre Clairambault , Peter Dybjer

Seely's paper "Locally cartesian closed categories and type theory" contains a well-known result in categorical type theory: that the category of locally cartesian closed categories is equivalent to the category … Seely's paper "Locally cartesian closed categories and type theory" contains a well-known result in categorical type theory: that the category of locally cartesian closed categories is equivalent to the category of Martin-L\"of type theories with Pi-types, Sigma-types and extensional identity types. However, Seely's proof relies on the problematic assumption that substitution in types can be interpreted by pullbacks. Here we prove a corrected version of Seely's theorem: that the B\'enabou-Hofmann interpretation of Martin-L\"of type theory in locally cartesian closed categories yields a biequivalence of 2-categories. To facilitate the technical development we employ categories with families as a substitute for syntactic Martin-L\"of type theories. As a second result we prove that if we remove Pi-types the resulting categories with families are biequivalent to left exact categories.

Chat View PDF