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

Author Description

Login to generate an author description

Ask a Question About This Mathematician

Towards a Directed Homotopy Type Theory

2019-11-01
Paige Randall North
In this paper, we present a directed homotopy type theory for reasoning synthetically about (higher) categories and directed homotopy theory. We specify a new 'homomorphism' type former for Martin-Löf type … In this paper, we present a directed homotopy type theory for reasoning synthetically about (higher) categories and directed homotopy theory. We specify a new 'homomorphism' type former for Martin-Löf type theory which is roughly analogous to the identity type former originally introduced by Martin-Löf. The homomorphism type former is meant to capture the notions of morphism (from the theory of categories) and directed path (from directed homotopy theory) just as the identity type former is known to capture the notions of isomorphism (from the theory of groupoids) and path (from homotopy theory). Our main result is an interpretation of these homomorphism types into Cat, the category of small categories. There, the interpretation of each homomorphism type homC(a,b) is indeed the set of morphisms between the objects a and b of the category C. We end the paper with an analysis of the interpretation in Cat with which we argue that our homomorphism types are indeed the directed version of Martin-Löf's identity types
View PDF Chat

A Higher Structure Identity Principle

2020-05-25
Benedikt Ahrens , Paige Randall North , Michael Shulman +1 more
The ordinary Structure Identity Principle states that any property of set-level structures (e.g., posets, groups, rings, fields) definable in Univalent Foundations is invariant under isomorphism: more specifically, identifications of structures … The ordinary Structure Identity Principle states that any property of set-level structures (e.g., posets, groups, rings, fields) definable in Univalent Foundations is invariant under isomorphism: more specifically, identifications of structures coincide with isomorphisms. We prove a version of this principle for a wide range of higher-categorical structures, adapting FOLDS-signatures to specify a general class of structures, and using two-level type theory to treat all categorical dimensions uniformly. As in the previously known case of 1-categories (which is an instance of our theory), the structures themselves must satisfy a local univalence principle, stating that identifications coincide with "isomorphisms" between elements of the structure. Our main technical achievement is a definition of such isomorphisms, which we call "indiscernibilities," using only the dependency structure rather than any notion of composition.
View PDF Chat

Univalent Foundations and the Equivalence Principle

2019-01-01
Benedikt Ahrens , Paige Randall North
View PDF Chat

Type theoretic weak factorization systems

2017-06-01
Paige Randall North
This article presents three characterizations of the weak factorization systems on finitely complete categories that interpret intensional dependent type theory with Sigma-, Pi-, and Id-types. The first characterization is that … This article presents three characterizations of the weak factorization systems on finitely complete categories that interpret intensional dependent type theory with Sigma-, Pi-, and Id-types. The first characterization is that the weak factorization system (L,R) has the properties that L is stable under pullback along R and that all maps to a terminal object are in R. We call such weak factorization systems type-theoretic. The second is that the weak factorization system has an Id-presentation: roughly, it is generated by Id-types in the empty context. The third is that the weak factorization system (L, R) is generated by a Moore relation system, a generalization of the notion of Moore paths.

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.

Semantics for two-dimensional type theory

2022-08-02
Benedikt Ahrens , Paige Randall North , Niels van der Weide
We propose a general notion of model for two-dimensional type theory, in the form of comprehension bicategories. Examples of comprehension bicategories are plentiful; they include interpretations of directed type theory … We propose a general notion of model for two-dimensional type theory, in the form of comprehension bicategories. Examples of comprehension bicategories are plentiful; they include interpretations of directed type theory previously studied in the literature.
View PDF Chat

Type-theoretic weak factorization systems

2019-01-01
Paige Randall North
This article presents three characterizations of the weak factorization systems on finitely complete categories that interpret intensional dependent type theory with Sigma-, Pi-, and Id-types. The first characterization is that … This article presents three characterizations of the weak factorization systems on finitely complete categories that interpret intensional dependent type theory with Sigma-, Pi-, and Id-types. The first characterization is that the weak factorization system (L,R) has the properties that L is stable under pullback along R and that all maps to a terminal object are in R. We call such weak factorization systems type-theoretic. The second is that the weak factorization system has an Id-presentation: roughly, it is generated by Id-types in the empty context. The third is that the weak factorization system (L, R) is generated by a Moore relation system, a generalization of the notion of Moore paths.

Towards a directed homotopy type theory

2018-07-27
Paige Randall North
In this paper, we present a directed homotopy type theory for reasoning synthetically about (higher) categories, directed homotopy theory, and its applications to concurrency. We specify a new `homomorphism' type … In this paper, we present a directed homotopy type theory for reasoning synthetically about (higher) categories, directed homotopy theory, and its applications to concurrency. We specify a new `homomorphism' type former for Martin-Lof type theory which is roughly analogous to the identity type former originally introduced by Martin-Lof. The homomorphism type former is meant to capture the notions of morphism (from the theory of categories) and directed path (from directed homotopy theory) just as the identity type former is known to capture the notions of isomorphism (from the theory of groupoids) and path (from homotopy theory). Our main result is an interpretation of these homomorphism types into Cat, the category of small categories. There, the interpretation of each homomorphism type hom(a,b) is indeed the set of morphisms between the objects a and b of a category C. We end the paper with an analysis of the interpretation in Cat with which we argue that our homomorphism types are indeed the directed version of Martin-Lof's identity types.

Identity types and weak factorization systems in Cauchy complete categories

2019-03-29
Paige Randall North
Abstract It has been known that categorical interpretations of dependent type theory with Σ- and Id -types induce weak factorization systems. When one has a weak factorization system $({\cal L},{\cal … Abstract It has been known that categorical interpretations of dependent type theory with Σ- and Id -types induce weak factorization systems. When one has a weak factorization system $({\cal L},{\cal R})$ on a category $\mathbb{C}$ in hand, it is then natural to ask whether or not $({\cal L},{\cal R})$ harbors an interpretation of dependent type theory with Σ- and Id - (and possibly Π-) types. Using the framework of display map categories to phrase this question more precisely, one would ask whether or not there exists a class ${\cal D}$ of morphisms of $\mathbb{C}$ such that the retract closure of ${\cal D}$ is the class ${\cal R}$ and the pair $(\mathbb{C},{\cal D})$ forms a display map category modeling Σ- and Id - (and possibly Π-) types. In this paper, we show, with the hypothesis that $\cal{C}$ is Cauchy complete, that there exists such a class $\cal{D}$ if and only if $(\mathbb{C},\cal{R})$ itself forms a display map category modeling Σ- and Id - (and possibly Π-) types. Thus, we reduce the search space of our original question from a potentially proper class to a singleton.
View PDF Chat

B-SYSTEMS AND C-SYSTEMS ARE EQUIVALENT

2023-06-29
Benedikt Ahrens , Jacopo Emmenegger , Paige Randall North +1 more
Abstract C-systems were defined by Cartmell as models of generalized algebraic theories. B-systems were defined by Voevodsky in his quest to formulate and prove an initiality conjecture for type theories. … Abstract C-systems were defined by Cartmell as models of generalized algebraic theories. B-systems were defined by Voevodsky in his quest to formulate and prove an initiality conjecture for type theories. They play a crucial role in Voevodsky’s construction of a syntactic C-system from a term monad. In this work, we construct an equivalence between the category of C-systems and the category of B-systems, thus proving a conjecture by Voevodsky.
View PDF Chat

Algebraic Presentations of Dependent Type Theories

2021-01-01
Benedikt Ahrens , Jacopo Emmenegger , Paige Randall North +1 more
C-systems were defined by Cartmell as models of generalized algebraic theories. B-systems were defined by Voevodsky in his quest to formulate and prove an initiality conjecture for type theories. They … C-systems were defined by Cartmell as models of generalized algebraic theories. B-systems were defined by Voevodsky in his quest to formulate and prove an initiality conjecture for type theories. They play a crucial role in Voevodsky's construction of a syntactic C-system from a term monad. In this work, we construct an equivalence between the category of C-systems and the category of B-systems, thus proving a conjecture by Voevodsky. We construct this equivalence as the restriction of an equivalence between more general structures, called CE-systems and E-systems, respectively. To this end, we identify C-systems and B-systems as "stratified" CE-systems and E-systems, respectively; that is, systems whose contexts are built iteratively via context extension, starting from the empty context.
View PDF Chat

Bicategorical type theory: semantics and syntax

2023-10-17
Benedikt Ahrens , Paige Randall North , Niels van der Weide
Abstract We develop semantics and syntax for bicategorical type theory. Bicategorical type theory features contexts, types, terms, and directed reductions between terms. This type theory is naturally interpreted in a … Abstract We develop semantics and syntax for bicategorical type theory. Bicategorical type theory features contexts, types, terms, and directed reductions between terms. This type theory is naturally interpreted in a class of structured bicategories. We start by developing the semantics, in the form of comprehension bicategories . Examples of comprehension bicategories are plentiful; we study both specific examples as well as classes of examples constructed from other data. From the notion of comprehension bicategory, we extract the syntax of bicategorical type theory, that is, judgment forms and structural inference rules. We prove soundness of the rules by giving an interpretation in any comprehension bicategory. The semantic aspects of our work are fully checked in the Coq proof assistant, based on the UniMath library.
View PDF Chat

Towards a Topological Model of Homotopy Type Theory

2015-01-01
Paige Randall North

A Hurewicz Model Structure for Directed Topology

2019-11-06
Sanjeevi Krishnan , Paige Randall North
This paper constructs an h-model structure for diagrams of streams, locally preordered spaces. Along the way, the paper extends some classical characterizations of Hurewicz fibrations and closed Hurewicz cofibrations. The … This paper constructs an h-model structure for diagrams of streams, locally preordered spaces. Along the way, the paper extends some classical characterizations of Hurewicz fibrations and closed Hurewicz cofibrations. The usual characterization of classical closed Hurewicz cofibrations as inclusions of neighborhood deformation retracts extends. A characterization of classical Hurewicz fibrations as algebras over a pointed Moore cocylinder endofunctor also extends. An immediate consequence is a long exact sequence for directed homotopy monoids, with applications to safety verifications for database protocols.

A Hurewicz model structure for directed topology

2021-06-08
Sanjeevi Krishnan , Paige Randall North
This paper constructs an h-model structure for diagrams of streams, locally preordered spaces. Along the way, the paper extends some classical characterizations of Hurewicz fibrations and closed Hurewicz cofibrations. The … This paper constructs an h-model structure for diagrams of streams, locally preordered spaces. Along the way, the paper extends some classical characterizations of Hurewicz fibrations and closed Hurewicz cofibrations. The usual characterization of classical closed Hurewicz cofibrations as inclusions of neighborhood deformation retracts extends. A characterization of classical Hurewicz fibrations as algebras over a pointed Moore cocylinder endofunctor also extends. An immediate consequence is a long exact sequence for directed homotopy monoids, with applications to safety verifications for database protocols.

B-systems and C-systems are equivalent

2021-11-18
Benedikt Ahrens , Jacopo Emmenegger , Paige Randall North +1 more
C-systems were defined by Cartmell as models of generalized algebraic theories. B-systems were defined by Voevodsky in his quest to formulate and prove an initiality conjecture for type theories. They … C-systems were defined by Cartmell as models of generalized algebraic theories. B-systems were defined by Voevodsky in his quest to formulate and prove an initiality conjecture for type theories. They play a crucial role in Voevodsky's construction of a syntactic C-system from a term monad. In this work, we construct an equivalence between the category of C-systems and the category of B-systems, thus proving a conjecture by Voevodsky.
View PDF Chat

A Hurewicz Model Structure for Directed Topology

2019-01-01
Sanjeevi Krishnan , Paige Randall North
This paper constructs an h-model structure for diagrams of streams, locally preordered spaces. Along the way, the paper extends some classical characterizations of Hurewicz fibrations and closed Hurewicz cofibrations. The … This paper constructs an h-model structure for diagrams of streams, locally preordered spaces. Along the way, the paper extends some classical characterizations of Hurewicz fibrations and closed Hurewicz cofibrations. The usual characterization of classical closed Hurewicz cofibrations as inclusions of neighborhood deformation retracts extends. A characterization of classical Hurewicz fibrations as algebras over a pointed Moore cocylinder endofunctor also extends. An immediate consequence is a long exact sequence for directed homotopy monoids, with applications to safety verifications for database protocols.
View PDF Chat

Towards a directed homotopy type theory

2018-01-01
Paige Randall North
In this paper, we present a directed homotopy type theory for reasoning synthetically about (higher) categories, directed homotopy theory, and its applications to concurrency. We specify a new `homomorphism' type … In this paper, we present a directed homotopy type theory for reasoning synthetically about (higher) categories, directed homotopy theory, and its applications to concurrency. We specify a new `homomorphism' type former for Martin-L\"of type theory which is roughly analogous to the identity type former originally introduced by Martin-L\"of. The homomorphism type former is meant to capture the notions of morphism (from the theory of categories) and directed path (from directed homotopy theory) just as the identity type former is known to capture the notions of isomorphism (from the theory of groupoids) and path (from homotopy theory). Our main result is an interpretation of these homomorphism types into Cat, the category of small categories. There, the interpretation of each homomorphism type hom(a,b) is indeed the set of morphisms between the objects a and b of a category C. We end the paper with an analysis of the interpretation in Cat with which we argue that our homomorphism types are indeed the directed version of Martin-L\"of's identity types.
View PDF Chat

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.

Coinductive control of inductive data types

2023-01-01
Paige Randall North , Maximilien Péroux
We combine the theory of inductive data types with the theory of universal measurings. By doing so, we find that many categories of algebras of endofunctors are actually enriched in … We combine the theory of inductive data types with the theory of universal measurings. By doing so, we find that many categories of algebras of endofunctors are actually enriched in the corresponding category of coalgebras of the same endofunctor. The enrichment captures all possible partial algebra homomorphisms, defined by measuring coalgebras. Thus this enriched category carries more information than the usual category of algebras which captures only total algebra homomorphisms. We specify new algebras besides the initial one using a generalization of the notion of initial algebra.
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

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

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

Measuring data types

2024-05-23
Lukas Mulder , Paige Randall North , Maximilien Péroux
In this article, we combine Sweedler's classic theory of measuring coalgebras -- by which $k$-algebras are enriched in $k$-coalgebras for $k$ a field -- with the theory of W-types -- … In this article, we combine Sweedler's classic theory of measuring coalgebras -- by which $k$-algebras are enriched in $k$-coalgebras for $k$ a field -- with the theory of W-types -- by which the categorical semantics of inductive data types in functional programming languages are understood. In our main theorem, we find that under some hypotheses, algebras of an endofunctor are enriched in coalgebras of the same endofunctor, and we find polynomial endofunctors provide many interesting examples of this phenomenon. We then generalize the notion of initial algebra of an endofunctor using this enrichment, thus generalizing the notion of W-type. This article is an extended version of arXiv:2303.16793, it adds expository introductions to the original theories of measuring coalgebras and W-types along with some improvements to the main theory and many explicitly worked examples.
View PDF Chat

Comparing Semantic Frameworks for Dependently-Sorted Algebraic Theories

2024-10-28
Benedikt Ahrens , Peter LeFanu Lumsdaine , Paige Randall North
View PDF Chat

Categorical Diffusion of Weighted Lattices

2025-01-07
Robert Ghrist , Rojas López , Paige Randall North +1 more
We introduce a categorical formalization of diffusion, motivated by data science and information dynamics. Central to our construction is the Lawvere Laplacian, an endofunctor on a product category indexed by … We introduce a categorical formalization of diffusion, motivated by data science and information dynamics. Central to our construction is the Lawvere Laplacian, an endofunctor on a product category indexed by a graph and enriched in a quantale. This framework permits the systematic study of diffusion processes on network sheaves taking values in a class of enriched categories.
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.

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.

Categorical Diffusion of Weighted Lattices

2025-01-07
Robert Ghrist , Rojas López , Paige Randall North +1 more
We introduce a categorical formalization of diffusion, motivated by data science and information dynamics. Central to our construction is the Lawvere Laplacian, an endofunctor on a product category indexed by … We introduce a categorical formalization of diffusion, motivated by data science and information dynamics. Central to our construction is the Lawvere Laplacian, an endofunctor on a product category indexed by a graph and enriched in a quantale. This framework permits the systematic study of diffusion processes on network sheaves taking values in a class of enriched categories.
View PDF Chat

Comparing Semantic Frameworks for Dependently-Sorted Algebraic Theories

2024-10-28
Benedikt Ahrens , Peter LeFanu Lumsdaine , Paige Randall North
View PDF Chat

Measuring data types

2024-05-23
Lukas Mulder , Paige Randall North , Maximilien Péroux
In this article, we combine Sweedler's classic theory of measuring coalgebras -- by which $k$-algebras are enriched in $k$-coalgebras for $k$ a field -- with the theory of W-types -- … In this article, we combine Sweedler's classic theory of measuring coalgebras -- by which $k$-algebras are enriched in $k$-coalgebras for $k$ a field -- with the theory of W-types -- by which the categorical semantics of inductive data types in functional programming languages are understood. In our main theorem, we find that under some hypotheses, algebras of an endofunctor are enriched in coalgebras of the same endofunctor, and we find polynomial endofunctors provide many interesting examples of this phenomenon. We then generalize the notion of initial algebra of an endofunctor using this enrichment, thus generalizing the notion of W-type. This article is an extended version of arXiv:2303.16793, it adds expository introductions to the original theories of measuring coalgebras and W-types along with some improvements to the main theory and many explicitly worked examples.
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

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

Bicategorical type theory: semantics and syntax

2023-10-17
Benedikt Ahrens , Paige Randall North , Niels van der Weide
Abstract We develop semantics and syntax for bicategorical type theory. Bicategorical type theory features contexts, types, terms, and directed reductions between terms. This type theory is naturally interpreted in a … Abstract We develop semantics and syntax for bicategorical type theory. Bicategorical type theory features contexts, types, terms, and directed reductions between terms. This type theory is naturally interpreted in a class of structured bicategories. We start by developing the semantics, in the form of comprehension bicategories . Examples of comprehension bicategories are plentiful; we study both specific examples as well as classes of examples constructed from other data. From the notion of comprehension bicategory, we extract the syntax of bicategorical type theory, that is, judgment forms and structural inference rules. We prove soundness of the rules by giving an interpretation in any comprehension bicategory. The semantic aspects of our work are fully checked in the Coq proof assistant, based on the UniMath library.
View PDF Chat

B-SYSTEMS AND C-SYSTEMS ARE EQUIVALENT

2023-06-29
Benedikt Ahrens , Jacopo Emmenegger , Paige Randall North +1 more
Abstract C-systems were defined by Cartmell as models of generalized algebraic theories. B-systems were defined by Voevodsky in his quest to formulate and prove an initiality conjecture for type theories. … Abstract C-systems were defined by Cartmell as models of generalized algebraic theories. B-systems were defined by Voevodsky in his quest to formulate and prove an initiality conjecture for type theories. They play a crucial role in Voevodsky’s construction of a syntactic C-system from a term monad. In this work, we construct an equivalence between the category of C-systems and the category of B-systems, thus proving a conjecture by Voevodsky.
View PDF Chat

Coinductive control of inductive data types

2023-01-01
Paige Randall North , Maximilien Péroux
We combine the theory of inductive data types with the theory of universal measurings. By doing so, we find that many categories of algebras of endofunctors are actually enriched in … We combine the theory of inductive data types with the theory of universal measurings. By doing so, we find that many categories of algebras of endofunctors are actually enriched in the corresponding category of coalgebras of the same endofunctor. The enrichment captures all possible partial algebra homomorphisms, defined by measuring coalgebras. Thus this enriched category carries more information than the usual category of algebras which captures only total algebra homomorphisms. We specify new algebras besides the initial one using a generalization of the notion of initial algebra.
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

Semantics for two-dimensional type theory

2022-08-02
Benedikt Ahrens , Paige Randall North , Niels van der Weide
We propose a general notion of model for two-dimensional type theory, in the form of comprehension bicategories. Examples of comprehension bicategories are plentiful; they include interpretations of directed type theory … We propose a general notion of model for two-dimensional type theory, in the form of comprehension bicategories. Examples of comprehension bicategories are plentiful; they include interpretations of directed type theory previously studied in the literature.
View PDF Chat

B-systems and C-systems are equivalent

2021-11-18
Benedikt Ahrens , Jacopo Emmenegger , Paige Randall North +1 more
C-systems were defined by Cartmell as models of generalized algebraic theories. B-systems were defined by Voevodsky in his quest to formulate and prove an initiality conjecture for type theories. They … C-systems were defined by Cartmell as models of generalized algebraic theories. B-systems were defined by Voevodsky in his quest to formulate and prove an initiality conjecture for type theories. They play a crucial role in Voevodsky's construction of a syntactic C-system from a term monad. In this work, we construct an equivalence between the category of C-systems and the category of B-systems, thus proving a conjecture by Voevodsky.
View PDF Chat

A Hurewicz model structure for directed topology

2021-06-08
Sanjeevi Krishnan , Paige Randall North
This paper constructs an h-model structure for diagrams of streams, locally preordered spaces. Along the way, the paper extends some classical characterizations of Hurewicz fibrations and closed Hurewicz cofibrations. The … This paper constructs an h-model structure for diagrams of streams, locally preordered spaces. Along the way, the paper extends some classical characterizations of Hurewicz fibrations and closed Hurewicz cofibrations. The usual characterization of classical closed Hurewicz cofibrations as inclusions of neighborhood deformation retracts extends. A characterization of classical Hurewicz fibrations as algebras over a pointed Moore cocylinder endofunctor also extends. An immediate consequence is a long exact sequence for directed homotopy monoids, with applications to safety verifications for database protocols.

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.

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.

Algebraic Presentations of Dependent Type Theories

2021-01-01
Benedikt Ahrens , Jacopo Emmenegger , Paige Randall North +1 more
C-systems were defined by Cartmell as models of generalized algebraic theories. B-systems were defined by Voevodsky in his quest to formulate and prove an initiality conjecture for type theories. They … C-systems were defined by Cartmell as models of generalized algebraic theories. B-systems were defined by Voevodsky in his quest to formulate and prove an initiality conjecture for type theories. They play a crucial role in Voevodsky's construction of a syntactic C-system from a term monad. In this work, we construct an equivalence between the category of C-systems and the category of B-systems, thus proving a conjecture by Voevodsky. We construct this equivalence as the restriction of an equivalence between more general structures, called CE-systems and E-systems, respectively. To this end, we identify C-systems and B-systems as "stratified" CE-systems and E-systems, respectively; that is, systems whose contexts are built iteratively via context extension, starting from the empty context.
View PDF Chat

A Higher Structure Identity Principle

2020-05-25
Benedikt Ahrens , Paige Randall North , Michael Shulman +1 more
The ordinary Structure Identity Principle states that any property of set-level structures (e.g., posets, groups, rings, fields) definable in Univalent Foundations is invariant under isomorphism: more specifically, identifications of structures … The ordinary Structure Identity Principle states that any property of set-level structures (e.g., posets, groups, rings, fields) definable in Univalent Foundations is invariant under isomorphism: more specifically, identifications of structures coincide with isomorphisms. We prove a version of this principle for a wide range of higher-categorical structures, adapting FOLDS-signatures to specify a general class of structures, and using two-level type theory to treat all categorical dimensions uniformly. As in the previously known case of 1-categories (which is an instance of our theory), the structures themselves must satisfy a local univalence principle, stating that identifications coincide with "isomorphisms" between elements of the structure. Our main technical achievement is a definition of such isomorphisms, which we call "indiscernibilities," using only the dependency structure rather than any notion of composition.
View PDF Chat

A Hurewicz Model Structure for Directed Topology

2019-11-06
Sanjeevi Krishnan , Paige Randall North
This paper constructs an h-model structure for diagrams of streams, locally preordered spaces. Along the way, the paper extends some classical characterizations of Hurewicz fibrations and closed Hurewicz cofibrations. The … This paper constructs an h-model structure for diagrams of streams, locally preordered spaces. Along the way, the paper extends some classical characterizations of Hurewicz fibrations and closed Hurewicz cofibrations. The usual characterization of classical closed Hurewicz cofibrations as inclusions of neighborhood deformation retracts extends. A characterization of classical Hurewicz fibrations as algebras over a pointed Moore cocylinder endofunctor also extends. An immediate consequence is a long exact sequence for directed homotopy monoids, with applications to safety verifications for database protocols.

Towards a Directed Homotopy Type Theory

2019-11-01
Paige Randall North
In this paper, we present a directed homotopy type theory for reasoning synthetically about (higher) categories and directed homotopy theory. We specify a new 'homomorphism' type former for Martin-Löf type … In this paper, we present a directed homotopy type theory for reasoning synthetically about (higher) categories and directed homotopy theory. We specify a new 'homomorphism' type former for Martin-Löf type theory which is roughly analogous to the identity type former originally introduced by Martin-Löf. The homomorphism type former is meant to capture the notions of morphism (from the theory of categories) and directed path (from directed homotopy theory) just as the identity type former is known to capture the notions of isomorphism (from the theory of groupoids) and path (from homotopy theory). Our main result is an interpretation of these homomorphism types into Cat, the category of small categories. There, the interpretation of each homomorphism type homC(a,b) is indeed the set of morphisms between the objects a and b of the category C. We end the paper with an analysis of the interpretation in Cat with which we argue that our homomorphism types are indeed the directed version of Martin-Löf's identity types
View PDF Chat

Identity types and weak factorization systems in Cauchy complete categories

2019-03-29
Paige Randall North
Abstract It has been known that categorical interpretations of dependent type theory with Σ- and Id -types induce weak factorization systems. When one has a weak factorization system $({\cal L},{\cal … Abstract It has been known that categorical interpretations of dependent type theory with Σ- and Id -types induce weak factorization systems. When one has a weak factorization system $({\cal L},{\cal R})$ on a category $\mathbb{C}$ in hand, it is then natural to ask whether or not $({\cal L},{\cal R})$ harbors an interpretation of dependent type theory with Σ- and Id - (and possibly Π-) types. Using the framework of display map categories to phrase this question more precisely, one would ask whether or not there exists a class ${\cal D}$ of morphisms of $\mathbb{C}$ such that the retract closure of ${\cal D}$ is the class ${\cal R}$ and the pair $(\mathbb{C},{\cal D})$ forms a display map category modeling Σ- and Id - (and possibly Π-) types. In this paper, we show, with the hypothesis that $\cal{C}$ is Cauchy complete, that there exists such a class $\cal{D}$ if and only if $(\mathbb{C},\cal{R})$ itself forms a display map category modeling Σ- and Id - (and possibly Π-) types. Thus, we reduce the search space of our original question from a potentially proper class to a singleton.
View PDF Chat

Univalent Foundations and the Equivalence Principle

2019-01-01
Benedikt Ahrens , Paige Randall North
View PDF Chat

A Hurewicz Model Structure for Directed Topology

2019-01-01
Sanjeevi Krishnan , Paige Randall North
This paper constructs an h-model structure for diagrams of streams, locally preordered spaces. Along the way, the paper extends some classical characterizations of Hurewicz fibrations and closed Hurewicz cofibrations. The … This paper constructs an h-model structure for diagrams of streams, locally preordered spaces. Along the way, the paper extends some classical characterizations of Hurewicz fibrations and closed Hurewicz cofibrations. The usual characterization of classical closed Hurewicz cofibrations as inclusions of neighborhood deformation retracts extends. A characterization of classical Hurewicz fibrations as algebras over a pointed Moore cocylinder endofunctor also extends. An immediate consequence is a long exact sequence for directed homotopy monoids, with applications to safety verifications for database protocols.
View PDF Chat

Type-theoretic weak factorization systems

2019-01-01
Paige Randall North
This article presents three characterizations of the weak factorization systems on finitely complete categories that interpret intensional dependent type theory with Sigma-, Pi-, and Id-types. The first characterization is that … This article presents three characterizations of the weak factorization systems on finitely complete categories that interpret intensional dependent type theory with Sigma-, Pi-, and Id-types. The first characterization is that the weak factorization system (L,R) has the properties that L is stable under pullback along R and that all maps to a terminal object are in R. We call such weak factorization systems type-theoretic. The second is that the weak factorization system has an Id-presentation: roughly, it is generated by Id-types in the empty context. The third is that the weak factorization system (L, R) is generated by a Moore relation system, a generalization of the notion of Moore paths.

Towards a directed homotopy type theory

2018-07-27
Paige Randall North
In this paper, we present a directed homotopy type theory for reasoning synthetically about (higher) categories, directed homotopy theory, and its applications to concurrency. We specify a new `homomorphism' type … In this paper, we present a directed homotopy type theory for reasoning synthetically about (higher) categories, directed homotopy theory, and its applications to concurrency. We specify a new `homomorphism' type former for Martin-Lof type theory which is roughly analogous to the identity type former originally introduced by Martin-Lof. The homomorphism type former is meant to capture the notions of morphism (from the theory of categories) and directed path (from directed homotopy theory) just as the identity type former is known to capture the notions of isomorphism (from the theory of groupoids) and path (from homotopy theory). Our main result is an interpretation of these homomorphism types into Cat, the category of small categories. There, the interpretation of each homomorphism type hom(a,b) is indeed the set of morphisms between the objects a and b of a category C. We end the paper with an analysis of the interpretation in Cat with which we argue that our homomorphism types are indeed the directed version of Martin-Lof's identity types.

Towards a directed homotopy type theory

2018-01-01
Paige Randall North
In this paper, we present a directed homotopy type theory for reasoning synthetically about (higher) categories, directed homotopy theory, and its applications to concurrency. We specify a new `homomorphism' type … In this paper, we present a directed homotopy type theory for reasoning synthetically about (higher) categories, directed homotopy theory, and its applications to concurrency. We specify a new `homomorphism' type former for Martin-L\"of type theory which is roughly analogous to the identity type former originally introduced by Martin-L\"of. The homomorphism type former is meant to capture the notions of morphism (from the theory of categories) and directed path (from directed homotopy theory) just as the identity type former is known to capture the notions of isomorphism (from the theory of groupoids) and path (from homotopy theory). Our main result is an interpretation of these homomorphism types into Cat, the category of small categories. There, the interpretation of each homomorphism type hom(a,b) is indeed the set of morphisms between the objects a and b of a category C. We end the paper with an analysis of the interpretation in Cat with which we argue that our homomorphism types are indeed the directed version of Martin-L\"of's identity types.
View PDF Chat

Type theoretic weak factorization systems

2017-06-01
Paige Randall North
This article presents three characterizations of the weak factorization systems on finitely complete categories that interpret intensional dependent type theory with Sigma-, Pi-, and Id-types. The first characterization is that … This article presents three characterizations of the weak factorization systems on finitely complete categories that interpret intensional dependent type theory with Sigma-, Pi-, and Id-types. The first characterization is that the weak factorization system (L,R) has the properties that L is stable under pullback along R and that all maps to a terminal object are in R. We call such weak factorization systems type-theoretic. The second is that the weak factorization system has an Id-presentation: roughly, it is generated by Id-types in the empty context. The third is that the weak factorization system (L, R) is generated by a Moore relation system, a generalization of the notion of Moore paths.

Towards a Topological Model of Homotopy Type Theory

2015-01-01
Paige Randall North
Coauthor Papers Together
Benedikt Ahrens 14
Niels van der Weide 5
Dimitris Tsementzis 4
Michael Shulman 4
Sanjeevi Krishnan 3
Nima Rasekh 3
Jacopo Emmenegger 3
Egbert Rijke 3
Maximilien Péroux 2
Lukas Mulder 1
Hans Riess 1
Rojas López 1
Robert Ghrist 1
Peter LeFanu Lumsdaine 1

The simplicial model of Univalent Foundations (after Voevodsky)

2021-03-08
Krzysztof 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-Löf type theory with one univalent universe (formulated in terms of contextual categories) is at least as consistent as ZFC with two inaccessible cardinals.
View PDF Chat

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 identity type weak factorisation system

2008-09-03
Nicola Gambino , Richard Garner
View PDF Chat

Type theoretic weak factorization systems

2017-06-01
Paige Randall North
This article presents three characterizations of the weak factorization systems on finitely complete categories that interpret intensional dependent type theory with Sigma-, Pi-, and Id-types. The first characterization is that … This article presents three characterizations of the weak factorization systems on finitely complete categories that interpret intensional dependent type theory with Sigma-, Pi-, and Id-types. The first characterization is that the weak factorization system (L,R) has the properties that L is stable under pullback along R and that all maps to a terminal object are in R. We call such weak factorization systems type-theoretic. The second is that the weak factorization system has an Id-presentation: roughly, it is generated by Id-types in the empty context. The third is that the weak factorization system (L, R) is generated by a Moore relation system, a generalization of the notion of Moore paths.

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

Topological and Simplicial Models of Identity Types

2012-01-01
Benno van den Berg , Richard Garner
In this paper we construct new categorical models for the identity types of Martin-Löf type theory, in the categories Top of topological spaces and SSet of simplicial sets. We do … In this paper we construct new categorical models for the identity types of Martin-Löf type theory, in the categories Top of topological spaces and SSet of simplicial sets. We do so building on earlier work of Awodey and Warren [2009], which has suggested that a suitable environment for the interpretation of identity types should be a category equipped with a weak factorization system in the sense of Bousfield--Quillen. It turns out that this is not quite enough for a sound model, due to some subtle coherence issues concerned with stability under substitution; and so our first task is to introduce a slightly richer structure, which we call a homotopy-theoretic model of identity types , and to prove that this is sufficient for a sound interpretation. Now, although both Top and SSet are categories endowed with a weak factorization system---and indeed, an entire Quillen model structure---exhibiting the additional structure required for a homotopy-theoretic model is quite hard to do. However, the categories we are interested in share a number of common features, and abstracting these leads us to introduce the notion of a path object category . This is a relatively simple axiomatic framework, which is nonetheless sufficiently strong to allow the construction of homotopy-theoretic models. Now by exhibiting suitable path object structures on Top and SSet , we endow those categories with the structure of a homotopy-theoretic model and, in this way, obtain the desired topological and simplicial models of identity types.
View PDF Chat

Premonoidal categories as categories with algebraic structure

2002-05-01
John Power

Abstract homotopy theory and generalized sheaf cohomology

1973-01-01
Kenneth S. Brown
Cohomology groups ${H^q}(X,E)$ are defined, where X is a topological space and E is a sheaf on X with values in Kan’s category of spectra. These groups generalize the ordinary … Cohomology groups ${H^q}(X,E)$ are defined, where X is a topological space and E is a sheaf on X with values in Kan’s category of spectra. These groups generalize the ordinary cohomology groups of X with coefficients in an abelian sheaf, as well as the generalized cohomology of X in the usual sense. The groups are defined by means of the “homotopical algebra” of Quillen applied to suitable categories of sheaves. The study of the homotopy category of sheaves of spectra requires an abstract homotopy theory more general than Quillen’s, and this is developed in Part I of the paper. Finally, the basic cohomological properties are proved, including a spectral sequence which generalizes the Atiyah-Hirzebruch spectral sequence (in generalized cohomology theory) and the “local to global” spectral sequence (in sheaf cohomology theory).
View PDF Chat

Towards a Categorical Foundation of Mathematics

2017-03-02
Michael Makkai
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.
View PDF Chat

Higher-Dimensional Algebra III.n-Categories and the Algebra of Opetopes

1998-05-01
John C. Baez , James G. Dolan

Structuralism, Invariance, and Univalence

2013-10-30
S. Awodey
Journal Article Structuralism, Invariance, and Univalence Get access Steve Awodey Steve Awodey * *Department of Philosophy, Carnegie Mellon University, Pittsburgh, Penn. 15213, U.S.A. [email protected]. The author is partly supported by … Journal Article Structuralism, Invariance, and Univalence Get access Steve Awodey Steve Awodey * *Department of Philosophy, Carnegie Mellon University, Pittsburgh, Penn. 15213, U.S.A. [email protected]. The author is partly supported by National Science Foundation grant DMS-1001191 and Air Force Office of Scientific Research grant 11NL035. Opinions, findings, conclusions or recommendations expressed here are those of the author and do not necessarily reflect the views of the NSF or AFOSR. Search for other works by this author on: Oxford Academic Google Scholar Philosophia Mathematica, Volume 22, Issue 1, February 2014, Pages 1–11, https://doi.org/10.1093/philmat/nkt030 Published: 30 October 2013
View PDF Chat

A Higher Structure Identity Principle

2020-05-25
Benedikt Ahrens , Paige Randall North , Michael Shulman +1 more
The ordinary Structure Identity Principle states that any property of set-level structures (e.g., posets, groups, rings, fields) definable in Univalent Foundations is invariant under isomorphism: more specifically, identifications of structures … The ordinary Structure Identity Principle states that any property of set-level structures (e.g., posets, groups, rings, fields) definable in Univalent Foundations is invariant under isomorphism: more specifically, identifications of structures coincide with isomorphisms. We prove a version of this principle for a wide range of higher-categorical structures, adapting FOLDS-signatures to specify a general class of structures, and using two-level type theory to treat all categorical dimensions uniformly. As in the previously known case of 1-categories (which is an instance of our theory), the structures themselves must satisfy a local univalence principle, stating that identifications coincide with "isomorphisms" between elements of the structure. Our main technical achievement is a definition of such isomorphisms, which we call "indiscernibilities," using only the dependency structure rather than any notion of composition.
View PDF Chat

Comprehension categories and the semantics of type dependency

1993-01-01
Bart Jacobs

Premonoidal categories and notions of computation

1997-10-01
John Power , E. Powell Robinson
We introduce the notions of premonoidal category and premonoidal functor, and show how these can be used in the denotational semantics of programming languages. We characterize the semantic definitions of … We introduce the notions of premonoidal category and premonoidal functor, and show how these can be used in the denotational semantics of programming languages. We characterize the semantic definitions of Eugenio Moggi's monads as notions of computation, exhibit a representation theorem for our premonoidal setting in terms of monads, and give a fibrational setting for the structure.

Higher Quasi-Categories vs Higher Rezk Spaces

2014-12-01
Dimitri Ara
We introduce a notion of n-quasi-categories as fibrant objects of a model category structure on presheaves on Joyal's n-cell category \Theta_n. Our definition comes from an idea of Cisinski and … We introduce a notion of n-quasi-categories as fibrant objects of a model category structure on presheaves on Joyal's n-cell category \Theta_n. Our definition comes from an idea of Cisinski and Joyal. However, we show that this idea has to be slightly modified to get a reasonable notion. We construct two Quillen equivalences between the model category of n-quasi-categories and the model category of Rezk \Theta_n-spaces showing that n-quasi-categories are a model for (\infty, n)-categories. For n = 1, we recover the two Quillen equivalences defined by Joyal and Tierney between quasi-categories and complete Segal spaces.
View PDF Chat

A cartesian presentation of weak<i>n</i>–categories

2010-01-02
Charles Rezk
A cartesian presentation of weak n-categories CHARLES REZKWe propose a notion of weak .nCk;n/-category, which we call .nCk;n/-‚-spaces.The .nCk; n/-‚-spaces are precisely the fibrant objects of a certain model category … A cartesian presentation of weak n-categories CHARLES REZKWe propose a notion of weak .nCk;n/-category, which we call .nCk;n/-‚-spaces.The .nCk; n/-‚-spaces are precisely the fibrant objects of a certain model category structure on the category of presheaves of simplicial sets on Joyal's category ‚ n .This notion is a generalization of that of complete Segal spaces (which are precisely the .1;1/-‚-spaces).Our main result is that the above model category is cartesian.18D05; 55U40 k is the full subcategory of fibrant objects in ‚ n Sp k ; equivalences in ‚ n Sp fib k are just levelwise weak equivalences of presheaves.
View PDF Chat

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

Homotopy theoretic models of identity types

2008-07-14
Steve Awodey , Michael A. Warren
This paper presents a novel connection between homotopical algebra and mathematical logic. It is shown that a form of intensional type theory is valid in any Quillen model category, generalizing … This paper presents a novel connection between homotopical algebra and mathematical logic. It is shown that a form of intensional type theory is valid in any Quillen model category, generalizing the Hofmann-Streicher groupoid model of Martin-Loef type theory.
View PDF Chat

Weak identity arrows in higher categories

2006-04-09
J.L.F. Kock
Journal Article Weak identity arrows in higher categories Get access Joachim Kock Joachim Kock Departament de Matemàtiques, Universitat Autònoma de Barcelona08193 Bellaterra (Barcelona), Spain E-mail address: [email protected] Search for other … Journal Article Weak identity arrows in higher categories Get access Joachim Kock Joachim Kock Departament de Matemàtiques, Universitat Autònoma de Barcelona08193 Bellaterra (Barcelona), Spain E-mail address: [email protected] Search for other works by this author on: Oxford Academic Google Scholar International Mathematics Research Papers, Volume 2006, 2006, 69163, https://doi.org/10.1155/IMRP/2006/69163 Published: 01 January 2006 Article history Received: 29 July 2005 Revision received: 28 November 2005 Accepted: 05 December 2005 Published: 01 January 2006
View PDF Chat

Towards a Categorical Foundation of Mathematics

1998-01-01
Michael Makkai
View PDF Chat

Univalence for inverse EI diagrams

2017-01-01
Michael Shulman
We construct a new model category presenting the homotopy theory of presheaves on "inverse EI (∞, 1)-categories", which contains universe objects that satisfy Voevodsky's univalence axiom.In addition to diagrams on … We construct a new model category presenting the homotopy theory of presheaves on "inverse EI (∞, 1)-categories", which contains universe objects that satisfy Voevodsky's univalence axiom.In addition to diagrams on ordinary inverse categories, as considered in previous work of the author, this includes a new model for equivariant algebraic topology with a compact Lie group of equivariance.Thus, it offers the potential for applications of homotopy type theory to equivariant homotopy theory.
View PDF Chat

Avoiding the axiom of choice in general category theory

1996-04-01
Michael Makkai

Univalence for inverse diagrams and homotopy canonicity

2014-11-24
Michael Shulman
We describe a homotopical version of the relational and gluing models of type theory, and generalize it to inverse diagrams and oplax limits. Our method uses the Reedy homotopy theory … We describe a homotopical version of the relational and gluing models of type theory, and generalize it to inverse diagrams and oplax limits. Our method uses the Reedy homotopy theory on inverse diagrams, and relies on the fact that Reedy fibrant diagrams correspond to contexts of a certain shape in type theory. This has two main applications. First, by considering inverse diagrams in Voevodsky's univalent model in simplicial sets, we obtain new models of univalence in a number of (∞, 1)-toposes; this answers a question raised at the Oberwolfach workshop on homotopical type theory. Second, by gluing the syntactic category of univalent type theory along its global sections functor to groupoids, we obtain a partial answer to Voevodsky's homotopy-canonicity conjecture: in 1-truncated type theory with one univalent universe of sets, any closed term of natural number type is homotopic to a numeral.
View PDF Chat

An experimental library of formalized Mathematics based on the univalent foundations

2015-01-20
Vladimir Voevodsky
This is a short overview of an experimental library of Mathematics formalized in the Coq proof assistant using the univalent interpretation of the underlying type theory of Coq. I started … This is a short overview of an experimental library of Mathematics formalized in the Coq proof assistant using the univalent interpretation of the underlying type theory of Coq. I started to work on this library in February 2010 in order to gain experience with formalization of Mathematics in a constructive type theory based on the intuition gained from the univalent models (see Kapulkin et al. 2012).
View PDF Chat

Understanding the Small Object Argument

2008-04-03
Richard Garner
View PDF Chat

The algebra of oriented simplexes

1987-12-01
Ross Street

On weak higher dimensional categories I: Part 1

2000-12-01
Claudio Hermida , Michael Makkai , John Power

Cauchy characterization of enriched categories

1981-12-01
Ross Street

Introduction to bicategories

1967-01-01
Jean Bénabou

Contravariance through enrichment

2016-01-01
Michael Shulman
We define strict and weak duality involutions on 2-categories, and prove a coherence theorem that every bicategory with a weak duality involution is biequivalent to a 2-category with a strict … We define strict and weak duality involutions on 2-categories, and prove a coherence theorem that every bicategory with a weak duality involution is biequivalent to a 2-category with a strict duality involution. For this purpose we introduce "2-categories with contravariance", a sort of enhanced 2-category with a basic notion of "contravariant morphism", which can be regarded either as generalized multicategories or as enriched categories. This enables a universal characterization of duality involutions using absolute weighted colimits, leading to a conceptual proof of the coherence theorem.

C-system of a module over a Jf-relative monad

2022-11-24
Vladimir Voevodsky
View PDF Chat

Subsystems and regular quotients of C-systems

2016-01-01
Vladimir Voevodsky
C-systems were introduced by J. Cartmell under the name contextual categories. In this note we study sub-objects and quotient-objects of C-systems. In the case of the sub-objects we consider all … C-systems were introduced by J. Cartmell under the name contextual categories. In this note we study sub-objects and quotient-objects of C-systems. In the case of the sub-objects we consider all sub-objects while in the case of the quotient-objects only {\em regular} quotients that in particular have the property that the corresponding projection morphism is surjective both on objects and on morphisms. It is one of several short papers based on the material of the Notes on Type Systems by the same author. This version is essentially identical with the version published in Contemporary Mathematics n.658.
View PDF Chat

Adjoint for double categories

2004-01-01
Marco Grandis , Robert Paré
Cet article poursuit notre etude de la theorie generale des categories doubles faibles, en traitant des adjonctions et des monades. Une adjonction double generale, telle qu'elle apparait dans des situations … Cet article poursuit notre etude de la theorie generale des categories doubles faibles, en traitant des adjonctions et des monades. Une adjonction double generale, telle qu'elle apparait dans des situations concretes, presente un foncteur double colax adjoint a gauche d'un foncteur double lax. Ce couple ne peut pas etre vu comme une adjonction dans une bicategorie, car les morphismes lax et colax n'en forment pas une. Mais ces adjonctions peuvent etre formalisees dans une categorie double interessante, formee des categories doubles faibles, avec les foncteurs doubles lax et colax comme fleches horizontales et verticales, et avec des cellules doubles convenables.

Stack semantics of type theory

2017-06-01
Thierry Coquand , Bassel Mannaa , Fabian Ruch
We give a model of dependent type theory with one univalent universe and propositional truncation interpreting a type as a stack, generalizing the groupoid model of type theory. As an … We give a model of dependent type theory with one univalent universe and propositional truncation interpreting a type as a stack, generalizing the groupoid model of type theory. As an application, we show that countable choice cannot be proved in dependent type theory with one univalent universe and propositional truncation.
View PDF Chat

Two-dimensional models of type theory

2009-07-02
Richard Garner
We describe a non-extensional variant of Martin-L\"of type theory which we call two-dimensional type theory, and equip it with a sound and complete semantics valued in 2-categories. We describe a non-extensional variant of Martin-L\"of type theory which we call two-dimensional type theory, and equip it with a sound and complete semantics valued in 2-categories.
View PDF Chat

A model structure on the category of pro-simplicial sets

2001-01-29
Daniel C. Isaksen
We study the category pro-<inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="script upper S script upper S"> <mml:semantics> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mi class="MJX-tex-caligraphic" mathvariant="script">S</mml:mi> <mml:mi class="MJX-tex-caligraphic" mathvariant="script">S</mml:mi> </mml:mrow> <mml:annotation encoding="application/x-tex">\mathcal {SS}</mml:annotation> </mml:semantics> </mml:math> </inline-formula> … We study the category pro-<inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="script upper S script upper S"> <mml:semantics> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mi class="MJX-tex-caligraphic" mathvariant="script">S</mml:mi> <mml:mi class="MJX-tex-caligraphic" mathvariant="script">S</mml:mi> </mml:mrow> <mml:annotation encoding="application/x-tex">\mathcal {SS}</mml:annotation> </mml:semantics> </mml:math> </inline-formula> of pro-simplicial sets, which arises in étale homotopy theory, shape theory, and pro-finite completion. We establish a model structure on pro-<inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="script upper S script upper S"> <mml:semantics> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mi class="MJX-tex-caligraphic" mathvariant="script">S</mml:mi> <mml:mi class="MJX-tex-caligraphic" mathvariant="script">S</mml:mi> </mml:mrow> <mml:annotation encoding="application/x-tex">\mathcal {SS}</mml:annotation> </mml:semantics> </mml:math> </inline-formula> so that it is possible to do homotopy theory in this category. This model structure is closely related to the strict structure of Edwards and Hastings. In order to understand the notion of homotopy groups for pro-spaces we use local systems on pro-spaces. We also give several alternative descriptions of weak equivalences, including a cohomological characterization. We outline dual constructions for ind-spaces.

Some properties of Fib as a fibred 2-category

1999-01-01
Claudio Hermida

Higher Operads, Higher Categories

2004-07-22
Tom Leinster
Higher-dimensional category theory is the study of n-categories, operads, braided monoidal categories, and other such exotic structures. It draws its inspiration from areas as diverse as topology, quantum algebra, mathematical … Higher-dimensional category theory is the study of n-categories, operads, braided monoidal categories, and other such exotic structures. It draws its inspiration from areas as diverse as topology, quantum algebra, mathematical physics, logic, and theoretical computer science. The heart of this book is the language of generalized operads. This is as natural and transparent a language for higher category theory as the language of sheaves is for algebraic geometry, or vector spaces for linear algebra. It is introduced carefully, then used to give simple descriptions of a variety of higher categorical structures. In particular, one possible definition of n-category is discussed in detail, and some common aspects of other possible definitions are established. This is the first book on the subject and lays its foundations. It will appeal to both graduate students and established researchers who wish to become acquainted with this modern branch of mathematics.
View PDF Chat

An Answer to Hellman's Question: ‘Does Category Theory Provide a Framework for Mathematical Structuralism?’†

2004-02-01
Steve Awodey
Journal Article An Answer to Hellman's Question: 'Does Category Theory Provide a Framework for Mathematical Structuralism?'† Get access STEVE AWODEY STEVE AWODEY *Department of Philosophy, Princeton University, Princeton, N. J. … Journal Article An Answer to Hellman's Question: 'Does Category Theory Provide a Framework for Mathematical Structuralism?'† Get access STEVE AWODEY STEVE AWODEY *Department of Philosophy, Princeton University, Princeton, N. J. 08544-1006 U. S. [email protected] Search for other works by this author on: Oxford Academic Google Scholar Philosophia Mathematica, Volume 12, Issue 1, February 2004, Pages 54–64, https://doi.org/10.1093/philmat/12.1.54 Published: 01 February 2004

Homotopy Type Theory: The Logic of Space

2021-03-22
Michael Shulman
This is an introduction to type theory, synthetic topology, and homotopy type theory from a category-theoretic and topological point of view, written as a chapter for the book New Spaces … This is an introduction to type theory, synthetic topology, and homotopy type theory from a category-theoretic and topological point of view, written as a chapter for the book New Spaces for Mathematics and Physics (ed. Gabriel Catren and Mathieu Anel).
View PDF Chat

Characterization of bicategories of stacks

1982-01-01
Ross Street

Metric, topology and multicategory—a common approach

2003-02-17
Maria Manuel Clementino , Walter Tholen

The Local Universes Model: An Overlooked Coherence Construction for Dependent Type Theories

2015-07-04
Peter LeFanu Lumsdaine , Michael A. Warren
We present a new coherence theorem for comprehension categories, providing strict models of dependent type theory with all standard constructors, including dependent products, dependent sums, identity types, and other inductive … We present a new coherence theorem for comprehension categories, providing strict models of dependent type theory with all standard constructors, including dependent products, dependent sums, identity types, and other inductive types. Precisely, we take as input a “weak model”: a comprehension category, equipped with structure corresponding to the desired logical constructions. We assume throughout that the base category is close to locally Cartesian closed: specifically, that products and certain exponentials exist. Beyond this, we require only that the logical structure should be weakly stable—a pure existence statement, not involving any specific choice of structure, weaker than standard categorical Beck--Chevalley conditions, and holding in the now standard homotopy-theoretic models of type theory. Given such a comprehension category, we construct an equivalent split one whose logical structure is strictly stable under reindexing. This yields an interpretation of type theory with the chosen constructors. The model is adapted from Voevodsky's use of universes for coherence, and at the level of fibrations is a classical construction of Giraud. It may be viewed in terms of local universes or delayed substitutions.
View PDF Chat

Combinatorial structure of type dependency

2014-10-16
Richard Garner
View PDF Chat

Une théorie combinatoire des séries formelles

1981-10-01
André Joyal

A model for the homotopy theory of homotopy theory

2000-06-20
Charles Rezk
We describe a category, the objects of which may be viewed as models for homotopy theories. We show that for such models, “functors between two homotopy theories form a homotopy … We describe a category, the objects of which may be viewed as models for homotopy theories. We show that for such models, “functors between two homotopy theories form a homotopy theory”, or more precisely that the category of such models has a well-behaved internal hom-object.

Fibrations and partial products in a 2-category

1993-01-01
Peter Johnstone

Categories for the Working Mathematician

1971-01-01
Saunders Mac Lane
View PDF Chat

Structure in Mathematics and Logic: A Categorical Perspective

1996-09-01
Steve Awodey
Abstract A precise notion of ‘mathematical structure’ other than that given by model theory may prove fruitful in the philosophy of mathematics. It is shown how the language and methods … Abstract A precise notion of ‘mathematical structure’ other than that given by model theory may prove fruitful in the philosophy of mathematics. It is shown how the language and methods of category theory provide such a notion, having developed out of a structural approach in modern mathematical practice. As an example, it is then shown how the categorical notion of a topos provides a characterization of ‘logical structure’, and an alternative to the Pregean approach to logic which is continuous with the modern structural approach in mathematics.

Cubical Approximation for Directed Topology I

2013-10-06
Sanjeevi Krishnan