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

Univalent Enriched Categories and the Enriched Rezk Completion

Authors

Niels van der Weide
Type: Preprint
Publication Date: 2024-01-01
Citations: 0
DOI: https://doi.org/10.48550/arxiv.2401.11752

Abstract

Enriched categories are categories whose sets of morphisms are enriched with extra structure. Such categories play a prominent role in the study of higher categories, homotopy theory, and the semantics of programming languages. In this paper, we study univalent enriched categories. We prove that all essentially surjective and fully faithful functors between univalent enriched categories are equivalences, and we show that every enriched category admits a Rezk completion. Finally, we use the Rezk completion for enriched categories to construct univalent enriched Kleisli categories.

Locations

  • arXiv (Cornell University)
    View
  • DataCite API
    View

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

Restriction categories as enriched categories

2013-12-24
Robin Cockett , Richard Garner
View PDF Chat

Univalent Categories and the Rezk Completion

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

Enriched infinity categories I: enriched presheaves

2020-01-01
John D. Berman
This is the first of a series of papers on enriched infinity categories, seeking to reduce enriched higher category theory to the higher algebra of presentable infinity categories, which is … This is the first of a series of papers on enriched infinity categories, seeking to reduce enriched higher category theory to the higher algebra of presentable infinity categories, which is better understood and can be approached via universal properties. In this paper, we introduce enriched presheaves on an enriched infinity category. We prove analogues of most familiar properties of presheaves. For example, we compute limits and colimits of presheaves, prove that all presheaves are colimits of representable presheaves, and prove a version of the Yoneda lemma.

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

A THEORY OF ENRICHED SKETCHES

1998-01-01
Francis Borceux , Carmen Quinteiro , Peter Johnstone
The theory of enriched accessible categories over a suitable base cate- gory V is developed. It is proved that these enriched accessible categories coincide with the categories of flat functors, … The theory of enriched accessible categories over a suitable base cate- gory V is developed. It is proved that these enriched accessible categories coincide with the categories of flat functors, but also with the categories of models of enriched sketches. A particular attention isdevoted to enriched locally presentable categoriesand enriched functors.

Enriched ∞-operads

2019-12-03
Hongyi Chu , Rune Haugseng

On bi-enriched $\infty$-categories

2024-06-14
Hadrian Heine
We extend Lurie's definition of enriched $\infty$-categories to notions of left enriched, right enriched and bi-enriched $\infty$-categories, which generalize the concepts of closed left tensored, right tensored and bitensored $\infty$-categories … We extend Lurie's definition of enriched $\infty$-categories to notions of left enriched, right enriched and bi-enriched $\infty$-categories, which generalize the concepts of closed left tensored, right tensored and bitensored $\infty$-categories and share many desirable features with them. We use bi-enriched $\infty$-categories to endow the $\infty$-category of enriched functors with enrichment that generalizes both the internal hom of the tensor product of enriched $\infty$-categories when the latter exists, and the free cocompletion under colimits and tensors. As an application we prove an end formula for morphism objects of enriched $\infty$-categories of enriched functors and compute the monad for enriched functors. We build our theory closely related to Lurie's higher algebra: we construct an enriched $\infty$-category of enriched presheaves via the enveloping tensored $\infty$-category, construct transfer of enrichment via scalar extension of bitensored $\infty$-categories, and construct enriched Kan-extensions via operadic Kan extensions. In particular, we develop an independent theory of enriched $\infty$-categories for Lurie's model of enriched $\infty$-categories.
View PDF Chat

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

Enriched functor categories

1969-01-01
Brian J. Day , G. M. Kelly

Kan extensions in Enriched Category Theory

1970-01-01
Eduardo J. Dubuc
View PDF Chat

Barr’s embedding theorem for enriched categories

2011-01-18
Dimitri Chikhladze
View PDF Chat

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

Enriched functor categories

2018-08-22
Stefan Schwede
A summary is not available for this content so a preview has been provided. Please use the Get access link above for information on how to access this content. A summary is not available for this content so a preview has been provided. Please use the Get access link above for information on how to access this content.

Enriched Sets and Higher Categories

2019-01-01
Bradley M. Willocks
We introduce the notion of an enriched set, as an abstraction of enriched categories, and a category of enriched sets. The set of enriched sets is itself described as a … We introduce the notion of an enriched set, as an abstraction of enriched categories, and a category of enriched sets. The set of enriched sets is itself described as a set enriched over the category of enriched sets. We introduce a method for the construction of sets enriched over the set of enriched sets from a given enriched set with some addition data, and for "functors" from such enriched sets as should thereby arise to the enriched set of enriched sets.

Enriched functor categories for functor calculus

2022-04-06
Lauren Bandklayder , Julia E. Bergner , Rhiannon Griffiths +2 more
View PDF Chat

Enriched functor categories for functor calculus

2020-01-01
Lauren Bandklayder , Julia E. Bergner , Rhiannon Griffiths +2 more
In this paper we present background results in enriched category theory and enriched model category theory necessary for developing model categories of enriched functors suitable for doing functor calculus. In this paper we present background results in enriched category theory and enriched model category theory necessary for developing model categories of enriched functors suitable for doing functor calculus.

Mealy Morphisms of Enriched Categories

2010-11-11
Robert Paré

Barr's Embedding Theorem for Enriched Categories

2009-01-01
Dimitri Chikhladze
We generalize Barr's embedding theorem for regular categories to the context of enriched categories. We generalize Barr's embedding theorem for regular categories to the context of enriched categories.