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

The internal languages of univalent categories

Authors

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

Abstract

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.

Locations

  • arXiv (Cornell University)
    View PDF

Ask a Question About This Paper

Summary

Login to see paper summary

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

The Formal Theory of Monads, Univalently

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

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.

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

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.

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

A Theory of Elementary Higher Toposes

2018-01-01
Nima Rasekh
We define an elementary $\infty$-topos that simultaneously generalizes an elementary topos and Grothendieck $\infty$-topos. We then prove it satisfies the expected topos theoretic properties, such as descent, local Cartesian closure, … We define an elementary $\infty$-topos that simultaneously generalizes an elementary topos and Grothendieck $\infty$-topos. We then prove it satisfies the expected topos theoretic properties, such as descent, local Cartesian closure, locality and classification of univalent morphisms, generalizing results by Lurie and Gepner-Kock. We also define $\infty$-logical functors and show the resulting $\infty$-category is closed under limits and filtered colimits, generalizing the analogous result for elementary toposes and Grothendieck $\infty$-toposes. Moreover, we give an alternative characterization of elementary $\infty$-toposes and their $\infty$-logical functors via their ind-completions. Finally we generalize these results by discussing the case of elementary (n,1)-toposes and give various examples and non-examples.
View PDF Chat

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

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.

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

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

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.

Modular correspondence between dependent type theories and categories including pretopoi and topoi

2005-12-08
Maria Emilia Maietti
We present a modular correspondence between various categorical structures and their internal languages in terms of extensional dependent type theories à la Martin-Löf. Starting from lex categories, through regular ones, … We present a modular correspondence between various categorical structures and their internal languages in terms of extensional dependent type theories à la Martin-Löf. Starting from lex categories, through regular ones, we provide internal languages of pretopoi and topoi and some variations of them, such as, for example, Heyting pretopoi.With respect to the internal languages already known for some of these categories, such as topoi, the novelty of these calculi is that formulas corresponding to subobjects can be regained as particular types that are equipped with proof-terms according to the isomorphism 'propositions as mono types', which was invisible in previously described internal languages.

Formal theory of internal categories

1996-12-01
Renato Betti
Categories internal to an elementary topos are regarded as monads in the bicategory of spans of the topos and the main features of the theory are developed: functors, adjointness, module … Categories internal to an elementary topos are regarded as monads in the bicategory of spans of the topos and the main features of the theory are developed: functors, adjointness, module calculus, internal presheaves, internal completeness and cocompleteness, Kan extensions.

Categories with Families: Unityped, Simply Typed, and Dependently Typed

2019-01-01
Simon Castellan , Pierre Clairambault , Peter Dybjer
We show how the categorical logic of untyped, simply typed and dependently typed lambda calculus can be structured around the notion of category with family (cwf). To this end we … We show how the categorical logic of untyped, simply typed and dependently typed lambda calculus can be structured around the notion of category with family (cwf). To this end we introduce subcategories of simply typed cwfs (scwfs), where types do not depend on variables, and unityped cwfs (ucwfs), where there is only one type. We prove several equivalence and biequivalence theorems between cwf-based notions and basic notions of categorical logic, such as cartesian operads, Lawvere theories, categories with finite products and limits, cartesian closed categories, and locally cartesian closed categories. Some of these theorems depend on the restrictions of contextuality (in the sense of Cartmell) or democracy (used by Clairambault and Dybjer for their biequivalence theorems). Some theorems are equivalences between notions with strict preservation of chosen structure. Others are biequivalences between notions where properties are only preserved up to isomorphism. In addition to this we discuss various constructions of initial ucwfs, scwfs, and cwfs with extra structure.
View PDF Chat

Categories with Families: Unityped, Simply Typed, and Dependently Typed

2019-04-01
Simon Castellan , Pierre Clairambault , Peter Dybjer
We show how the categorical logic of untyped, simply typed and dependently typed lambda calculus can be structured around the notion of category with family (cwf). To this end we … We show how the categorical logic of untyped, simply typed and dependently typed lambda calculus can be structured around the notion of category with family (cwf). To this end we introduce subcategories of simply typed cwfs (scwfs), where types do not depend on variables, and unityped cwfs (ucwfs), where there is only one type. We prove several equivalence and biequivalence theorems between cwf-based notions and basic notions of categorical logic, such as cartesian operads, Lawvere theories, categories with finite products and limits, cartesian closed categories, and locally cartesian closed categories. Some of these theorems depend on the restrictions of contextuality (in the sense of Cartmell) or democracy (used by Clairambault and Dybjer for their biequivalence theorems). Some theorems are equivalences between notions with strict preservation of chosen structure. Others are biequivalences between notions where properties are only preserved up to isomorphism. In addition to this we discuss various constructions of initial ucwfs, scwfs, and cwfs with extra structure.

Limits and colimits in internal higher category theory

2021-01-01
Louis Martini , Sebastián Wolf
We develop a number of basic concepts in the theory of categories internal to an $\infty$-topos. We discuss adjunctions, limits and colimits as well as Kan extensions for internal categories, … We develop a number of basic concepts in the theory of categories internal to an $\infty$-topos. We discuss adjunctions, limits and colimits as well as Kan extensions for internal categories, and we use these results to prove the universal property of internal presheaf categories. We furthermore construct the free cocompletion of an internal category by colimits that are indexed by an arbitrary class of diagram shapes.
View PDF Chat

Limits and colimits in internal higher category theory

2021-11-29
Louis Martini , S. Wolf
We develop a number of basic concepts in the theory of categories internal to an $\infty$-topos. We discuss adjunctions, limits and colimits as well as Kan extensions for internal categories, … We develop a number of basic concepts in the theory of categories internal to an $\infty$-topos. We discuss adjunctions, limits and colimits as well as Kan extensions for internal categories, and we use these results to prove the universal property of internal presheaf categories. We furthermore construct the free cocompletion of an internal category by colimits that are indexed by an arbitrary class of diagram shapes.

Categories with families, FOLDS and logic enriched type theory

2016-05-05
Erik Palmgren
Categories with families (cwfs) is an established semantical structure for dependent type theories, such as Martin-Lo type theory. Makkai's first-order logic with dependent sorts (FOLDS) is an example of a … Categories with families (cwfs) is an established semantical structure for dependent type theories, such as Martin-Lo type theory. Makkai's first-order logic with dependent sorts (FOLDS) is an example of a so-called logic enriched type theory. We introduce in this article a notion of hyperdoctrine over a cwf, and show how FOLDS and Aczel's and Belo's dependently typed (intuitionistic) first-order logic (DFOL) fit in this semantical framework. A soundness and completeness theorem is proved for such a logic. The semantics is functorial in the sense of Lawvere, and uses a dependent version of the Lindenbaum-Tarski algebra for a DFOL theory. Agreement with standard first-order semantics is established. Some applications of DFOL to constructive mathematics and categorical foundations are given. A key feature is a local propositions-as-types principle.