SU\G(𝔸)/K·U
Sign Up for free Log In

Insights From Univalent Foundations: A Case Study Using Double Categories

Authors

Nima Rasekh, Niels van der Weide, Benedikt Ahrens, Paige Randall North
Type: Preprint
Publication Date: 2024-02-07
Citations: 0
DOI: https://doi.org/10.48550/arxiv.2402.05265

Abstract

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

Locations

  • arXiv (Cornell University)
    View PDF

Ask a Question About This Paper

Summary

Login to see paper summary

Univalent Double Categories

2024-01-09
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.
View PDF Chat

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
View PDF Chat

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.
View PDF Chat

Univalent Categories and the Rezk Completion

2015-01-01
Benedikt Ahrens , Krzysztof Kapulkin , Michael Shulman
View PDF Chat

Bicategories in Univalent Foundations

2019-03-04
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, 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.

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.
View PDF Chat

Univalent Monoidal Categories

2023-07-28
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.
View PDF Chat

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.

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.
View PDF Chat

Categories of categories

2022-10-13
Eugenia Cheng
We gather small categories and functors into a category Cat, taking care with size issues to avoid a Russell-like paradox. We consider some functors from Cat to Set, and to … We gather small categories and functors into a category Cat, taking care with size issues to avoid a Russell-like paradox. We consider some functors from Cat to Set, and to the category of graphs and their morphisms. We sketch a free category functor. We look at structures in Cat, much as we have done with other examples of large categories of mathematical structures. We examine terminal and initial objects in Cat, then products and coproducts, and the relationship between (co)products in Cat and those in the categories of posets or monoids. We examine isomorphisms in Cat and show that these exhibit categories with the same arrow structure, such as the cube of factors of 30 and the cube of three types of privilege. We discuss the fact that this concept is overly strict, as it invokes equalities between objects, showing that Cat strains at its dimensions and is trying to expand into higher dimensions. This leads us to the definition of full, faithful, and essentially surjective. We show that full and faithful functors reflect isomorphisms. We define pointwise equivalence and discuss the sense in which this is a version of bijection, not of isomorphism.

Categories and Functors

2017-01-01
Alexey L. Gorodentsev

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.
View PDF Chat

The Univalence Principle

2025-01-14
Benedikt Ahrens , Paige Randall North , Michael Shulman +1 more
The Univalence Principle is the statement that equivalent mathematical structures are indistinguishable. We prove a general version of this principle that applies to all set-based, categorical, and higher-categorical structures defined … The Univalence Principle is the statement that equivalent mathematical structures are indistinguishable. We prove a general version of this principle that applies to all set-based, categorical, and higher-categorical structures defined in a non-algebraic and space-based style, as well as models of higher-order theories such as topological spaces. In particular, we formulate a general definition of indiscernibility for objects of any such structure, and a corresponding univalence condition that generalizes Rezk’s completeness condition for Segal spaces and ensures that all equivalences of structures are levelwise equivalences. Our work builds on Makkai’s First-Order Logic with Dependent Sorts, but is expressed in Voevodsky’s Univalent Foundations (UF), extending previous work on the Structure Identity Principle and univalent categories in UF. This enables indistinguishability to be expressed simply as identification, and yields a formal theory that is interpretable in classical homotopy theory, but also in other higher topos models. It follows that Univalent Foundations is a fully equivalence-invariant foundation for higher-categorical mathematics, as intended by Voevodsky.

Categories: the idea

2022-10-13
Eugenia Cheng
An overview of what the point of category theory is, without formality, and an overview of the contents of the book. We will present category theory as “the mathematics of … An overview of what the point of category theory is, without formality, and an overview of the contents of the book. We will present category theory as “the mathematics of mathematics”, so first we explain what aspects of mathematics we are focusing on. We present mathematics as starting from abstraction, as a way of elucidating analogies between situations, finding connections between them, and unifying them. Category theory is then a rigorous framework for making analogies and finding connections between different parts of mathematics. It focuses on relationships between things, rather than on intrinsic characteristics, and uses those relationships to put objects in context rather than treat them in isolation. Once the framework has been set up, we have, among other things, a way to express more nuanced notions of “sameness”, and a way to characterize things by the role they play in that context. Category theory also works at many different levels, so we can zoom in and out and study details close up, or broad contexts with more of an overview.

Homotopy Type Theory: A Synthetic Approach to Higher Equalities

2018-01-18
Michael Shulman
Homotopy type theory and univalent foundations (HoTT/UF) is a new foundation of mathematics, based not on set theory but on “infinity-groupoids”, which consist of collections of objects, ways in which … Homotopy type theory and univalent foundations (HoTT/UF) is a new foundation of mathematics, based not on set theory but on “infinity-groupoids”, which consist of collections of objects, ways in which two objects can be equal, ways in which those ways-to-be-equal can be equal, ad infinitum. Though apparently complicated, such structures are increasingly important in mathematics. Philosophically, they are an inevitable result of the notion that whenever we form a collection of things, we must simultaneously consider when two of those things are the same. The “synthetic” nature of HoTT/UF enables a much simpler description of infinity groupoids than is available in set theory, thereby aligning with modern mathematics while placing “equality” back in the foundations of logic. This chapter will introduce the basic ideas of HoTT/UF for a philosophical audience, including Voevodsky’s univalence axiom and higher inductive types.
View PDF Chat

Infinity category theory from scratch

2020-02-11
Emily Riehl , Dominic Verity
These lecture notes were written to accompany a mini course given at the 2015 Young Topologists' Meeting at Ecole Polytechnique Federale de Lausanne, videos of which can be found here … These lecture notes were written to accompany a mini course given at the 2015 Young Topologists' Meeting at Ecole Polytechnique Federale de Lausanne, videos of which can be found here . We use the terms ∞-categories and ∞-functors to mean the objects and morphisms in an ∞-cosmos: a simplicially enriched category satisfying a few axioms, reminiscent of an enriched category of fibrant objects. Quasi-categories, Segal categories, complete Segal spaces, naturally marked simplicial sets, iterated complete Segal spaces, Θ n -spaces, and fibered versions of each of these are all ∞-categories in this sense. We show that the basic category theory of ∞-categories and ∞-functors can be developed from the axioms of an ∞-cosmos; indeed, most of the work is internal to a strict 2-category of ∞-categories, ∞-functors, and natural transformations. In the ∞-cosmos of quasi-categories, we recapture precisely the same category theory developed by Joyal and Lurie, although in most cases our definitions, which are 2-categorical rather than combinatorial in nature, present a new incarnation of the standard concepts. In the first lecture, we define an ∞-cosmos and introduce its homotopy 2-category, the strict 2-category mentioned above. We illustrate the use of formal category theory to develop the basic theory of equivalences of and adjunctions between ∞-categories. In the second lecture, we study limits and colimits of diagrams taking values in an ∞-category and relate these concepts to adjunctions between ∞-categories. In the third lecture, we define comma ∞-categories, which satisfy a particular weak 2-dimensional universal property in the homotopy 2-category. We illustrate the use of comma ∞-categories to encode the universal properties of (co)limits and adjointness. Because comma ∞-categories are preserved by all functors of ∞-cosmoi and created by certain weak equivalences of ∞-cosmoi, these characterizations form the foundations for model independence'' results. In the fourth lecture, we introduce (co)cartesian fibrations, a certain class of ∞-functors, and also consider the special case with groupoidal fibers. We then describe the calculus of modules between ∞-categories --- comma ∞-categories being the prototypical example --- and use this framework to state and prove the Yoneda lemma and develop the theory of pointwise Kan extensions of ∞-functors.

The Double Category of Paired Dialgebras on the Chu Category

2018-12-18
Aydin Manzouri
The scientific and practical needs of the twenty-first century lead humankind to convergence of the specialized and diverse branches of science and technology. This convergence reveals the need for new … The scientific and practical needs of the twenty-first century lead humankind to convergence of the specialized and diverse branches of science and technology. This convergence reveals the need for new mathematical theories capable of providing common languages and frameworks to be utilized by professionals from different fileds in solving interdisciplinary and challenging problems. The present thesis is done in the same direction. Here, we develop a new formalism with the central idea of unification of various mathematical branches. For this purpose, we utilize three major tools from today's mathematics, each of which possessing a unifying nature itself: category theory and especially the theory of cateogries, the theory of universal dialgebra, and the Chu construction. With the aid of these tools, we define and study a double category that subsumes a significant portion of the formalisms usual within the body of mathematics and theoretical computer science. We show that this double category possesses the properties of self-duality and vertical self-duality. Also, we perform a primary investigation about existence of binary horizontal products and coproducts in this category. Finally, we give some suggestions for future work.

The Univalence Principle

2021-01-01
Benedikt Ahrens , Paige Randall North , Michael Shulman +1 more
The Univalence Principle is the statement that equivalent mathematical structures are indistinguishable. We prove a general version of this principle that applies to all set-based, categorical, and higher-categorical structures defined … The Univalence Principle is the statement that equivalent mathematical structures are indistinguishable. We prove a general version of this principle that applies to all set-based, categorical, and higher-categorical structures defined in a non-algebraic and space-based style, as well as models of higher-order theories such as topological spaces. In particular, we formulate a general definition of indiscernibility for objects of any such structure, and a corresponding univalence condition that generalizes Rezk's completeness condition for Segal spaces and ensures that all equivalences of structures are levelwise equivalences. Our work builds on Makkai's First-Order Logic with Dependent Sorts, but is expressed in Voevodsky's Univalent Foundations (UF), extending previous work on the Structure Identity Principle and univalent categories in UF. This enables indistinguishability to be expressed simply as identification, and yields a formal theory that is interpretable in classical homotopy theory, but also in other higher topos models. It follows that Univalent Foundations is a fully equivalence-invariant foundation for higher-categorical mathematics, as intended by Voevodsky.

The Univalence Principle.

2021-02-11
Benedikt Ahrens , Paige Randall North , Michael Shulman +1 more
The Univalence Principle is the statement that equivalent mathematical structures are indistinguishable. We prove a general version of this principle that applies to all set-based, categorical, and higher-categorical structures defined … The Univalence Principle is the statement that equivalent mathematical structures are indistinguishable. We prove a general version of this principle that applies to all set-based, categorical, and higher-categorical structures defined in a non-algebraic and space-based style, as well as models of higher-order theories such as topological spaces. In particular, we formulate a general definition of indiscernibility for objects of any such structure, and a corresponding univalence condition that generalizes Rezk's completeness condition for Segal spaces and ensures that all equivalences of structures are levelwise equivalences. Our work builds on Makkai's First-Order Logic with Dependent Sorts, but is expressed in Voevodsky's Univalent Foundations (UF), extending previous work on the Structure Identity Principle and univalent categories in UF. This enables indistinguishability to be expressed simply as identification, and yields a formal theory that is interpretable in classical homotopy theory, but also in other higher topos models. It follows that Univalent Foundations is a fully equivalence-invariant foundation for higher-categorical mathematics, as intended by Voevodsky.