Towards a Directed Homotopy Type Theory

Authors

Paige Randall North

Type: Article

Publication Date: 2019-11-01

Citations: 15

DOI: https://doi.org/10.1016/j.entcs.2019.09.012

View Ask PDF

Abstract

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

Locations

arXiv (Cornell University)
View PDF
Utrecht University Repository (Utrecht University)
View PDF
Electronic Notes in Theoretical Computer Science
View

Ask a Question About This Paper

Summary

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

Modeling Martin-Löf type theory in categories

2013-09-04

F. Lamarche

We present a model of Martin-Löf type theory that includes both dependent products and the identity type. It is based on the category of small categories, with cloven Grothendieck bifibrations … We present a model of Martin-Löf type theory that includes both dependent products and the identity type. It is based on the category of small categories, with cloven Grothendieck bifibrations used to model dependent types. The identity type is modeled by a path functor that seems to have independent interest from the point of view of homotopy theory. We briefly describe this modelʼs strengths and limitations.

View PDF Chat

Path Functors in Cat

2013-09-19

F. Lamarche

We build an endofunctor in the category of small categories along with the necessary structure on it to turn it into a path object suitable for homotopy theory and modelling … We build an endofunctor in the category of small categories along with the necessary structure on it to turn it into a path object suitable for homotopy theory and modelling identity types in Martin-L of type theory. We construct the free Grothendieck bifibration over a base category generated by an arbitrary functor to that category.

Homotopy in Cat via Paths and the Fundamental Groupoid of a Category

2008-01-01

F. Lamarche

We construct an endofunctor of paths in the category of small category and show how to construct the standard homotopy invariants from it. We give a novel proof that the … We construct an endofunctor of paths in the category of small category and show how to construct the standard homotopy invariants from it. We give a novel proof that the fundamental groupoid of a category is its associated universal groupoid.

Directed univalence in simplicial homotopy type theory

2024-07-12

Daniel Gratzer , Jonathan Weinberger , Ulrik Buchholtz

Simplicial type theory extends homotopy type theory with a directed path type which internalizes the notion of a homomorphism within a type. This concept has significant applications both within mathematics … Simplicial type theory extends homotopy type theory with a directed path type which internalizes the notion of a homomorphism within a type. This concept has significant applications both within mathematics -- where it allows for synthetic (higher) category theory -- and programming languages -- where it leads to a directed version of the structure identity principle. In this work, we construct the first types in simplicial type theory with non-trivial homomorphisms. We extend simplicial type theory with modalities and new reasoning principles to obtain triangulated type theory in order to construct the universe of discrete types $\mathcal{S}$. We prove that homomorphisms in this type correspond to ordinary functions of types i.e., that $\mathcal{S}$ is directed univalent. The construction of $\mathcal{S}$ is foundational for both of the aforementioned applications of simplicial type theory. We are able to define several crucial examples of categories and to recover important results from category theory. Using $\mathcal{S}$, we are also able to define various types whose usage is guaranteed to be functorial. These provide the first complete examples of the proposed directed structure identity principle.

View PDF Chat

The Directed Homotopy Hypothesis

2016-09-01

Jérémy Dubut , Éric Goubault , Jean Goubault-Larrecq

The homotopy hypothesis was originally stated by Grothendieck: topological spaces should be equivalent to (weak) infinite-groupoids, which give algebraic representatives of homotopy types. Much later, several authors developed geometrizations of … The homotopy hypothesis was originally stated by Grothendieck: topological spaces should be equivalent to (weak) infinite-groupoids, which give algebraic representatives of homotopy types. Much later, several authors developed geometrizations of computational models, e.g., for rewriting, distributed systems, (homotopy) type theory etc. But an essential feature in the work set up in concurrency theory, is that time should be considered irreversible, giving rise to the field of directed algebraic topology. Following the path proposed by Porter, we state here a directed homotopy hypothesis: Grandis' directed topological spaces should be equivalent to a weak form of topologically enriched categories, still very close to (infinite,1)-categories. We develop, as in ordinary algebraic topology, a directed homotopy equivalence and a weak equivalence, and show invariance of a form of directed homology.

View PDF Chat

Six model categories for directed homotopy

2019-04-23

Philippe Gaucher

View PDF Chat

Categories of categories

2022-10-13

Eugenia Cheng

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

THE SHAPE OF A CATEGORY UP TO DIRECTED HOMOTOPY

2005-01-01

Marco Grandis

This work is a contribution to a recent field, Directed Algebraic Topology. Categories which appear as fundamental categories of ‘directed structures’, e.g. ordered topological spaces, have to be studied up … This work is a contribution to a recent field, Directed Algebraic Topology. Categories which appear as fundamental categories of ‘directed structures’, e.g. ordered topological spaces, have to be studied up to appropriate notions of directed homotopy equivalence, which are more general than ordinary equivalence of categories. Here we introduce past and future equivalences of categories—sort of symmetric versions of an adjunction—and use them and their combinations to get ‘directed models’ of a category; in the simplest case, these are the join of the least full reflective and the least full coreflective subcategory.

Advancing categories with functors of functors

2023-03-28

Pierros Ntelis

In this document, we review the basics of category theory and functors calculus, and we implement some novel concepts. In particular, we review the concepts of category, functors, and natural … In this document, we review the basics of category theory and functors calculus, and we implement some novel concepts. In particular, we review the concepts of category, functors, and natural transformations. Furthermore we introduce the novel concept of func- tors of functors. We illustrate these concepts with diagrams to ameliorate the expression of these ideas. We conclude that these concepts open new avenues and are advancing category.

View PDF Chat

Directed Containers as Categories

2016-04-01

Danel Ahman , Tarmo Uustalu

Directed containers make explicit the additional structure of those containers whose set functor interpretation carries a comonad structure. The data and laws of a directed container resemble those of a … Directed containers make explicit the additional structure of those containers whose set functor interpretation carries a comonad structure. The data and laws of a directed container resemble those of a monoid, while the data and laws of a directed container morphism those of a monoid morphism in the reverse direction. With some reorganization, a directed container is the same as a small category, but a directed container morphism is opcleavage-like. We draw some conclusions for comonads from this observation, considering in particular basic constructions and concepts like the opposite category and a groupoid.

View PDF Chat

Autonomous categories and duality of functors

1965-09-01

F. E. J. Linton

Modelling fundamental 2-categories for directed homotopy

2006-01-01

Marco Grandis

Directed Algebraic Topology is a recent field, deeply linked with ordinary and higher dimensional Category Theory.A 'directed space', e.g. an ordered topological space, has directed homotopies (which are generally non-reversible) … Directed Algebraic Topology is a recent field, deeply linked with ordinary and higher dimensional Category Theory.A 'directed space', e.g. an ordered topological space, has directed homotopies (which are generally non-reversible) and fundamental n-categories (replacing the fundamental n-groupoids of the classical case).Finding a simple model of the latter is a nontrivial problem, whose solution gives relevant information on the given 'space'; a problem which is also of interest in general Category Theory, as it requires equivalence relations which are more general than categorical equivalence.Taking on a previous work on 'The shape of a category up to directed homotopy', we study now the fundamental 2-category of a directed space.All the notions of 2-category theory used here are explicitly reviewed.

View PDF Chat

Eilenberg-MacLane spaces in homotopy type theory

2014-07-14

Daniel R. Licata , Eric Finster

Homotopy type theory is an extension of Martin-Löf type theory with principles inspired by category theory and homotopy theory. With these extensions, type theory can be used to construct proofs … Homotopy type theory is an extension of Martin-Löf type theory with principles inspired by category theory and homotopy theory. With these extensions, type theory can be used to construct proofs of homotopy-theoretic theorems, in a way that is very amenable to computer-checked proofs in proof assistants such as Coq and Agda. In this paper, we give a computer-checked construction of Eilenberg-MacLane spaces. For an abelian group G, an Eilenberg-MacLane space K(G,n) is a space (type) whose nth homotopy group is G, and whose homotopy groups are trivial otherwise. These spaces are a basic tool in algebraic topology; for example, they can be used to build spaces with specified homotopy groups, and to define the notion of cohomology with coefficients in G. Their construction in type theory is an illustrative example, which ties together many of the constructions and methods that have been used in homotopy type theory so far.

View PDF Chat

Synthetic 1-Categories in Directed Type Theory

2024-10-25

Thorsten Altenkirch , J. v. Neumann

The field of directed type theory seeks to design type theories capable of reasoning synthetically about (higher) categories, by generalizing the symmetric identity types of Martin-L\"of Type Theory to asymmetric … The field of directed type theory seeks to design type theories capable of reasoning synthetically about (higher) categories, by generalizing the symmetric identity types of Martin-L\"of Type Theory to asymmetric hom-types. We articulate the directed type theory of the category model, with appropriate modalities for keeping track of variances and a powerful directed-J rule capable of proving results about arbitrary terms of hom-types; we put this rule to use in making several constructions in synthetic 1-category theory. Because this theory is expressed entirely in terms of generalized algebraic theories, we know automatically that this directed type theory admits a syntax model and is the first step towards directed higher observational type theory.

View PDF Chat

An Introduction to Higher Categories

2019-01-01

Simona Paoli

Computational Paths and the Fundamental Groupoid of a Type

2021-07-16

Arthur Ramos , Ruy J. G. B. de Queiroz , Anjolina G. de Oliveira

Using computational paths as the fundamental concept, we show that we can leverage Category Theory to propose the concept of fundamental groupoid of a type. Using computational paths as the fundamental concept, we show that we can leverage Category Theory to propose the concept of fundamental groupoid of a type.

View PDF Chat

From Morphism Categories to Functor Categories

2025-04-22

Rasool Hafezi , Hossein Eshraghi

Categories and Functors

2017-01-01

Alexey L. Gorodentsev

Formalizing the ∞-Categorical Yoneda Lemma

2024-01-09

Nikolai Kudasov , Emily Riehl , Jonathan Weinberger

Formalized 1-category theory forms a core component of various libraries of mathematical proofs. However, more sophisticated results in fields from algebraic topology to theoretical physics, where objects have "higher structure," … Formalized 1-category theory forms a core component of various libraries of mathematical proofs. However, more sophisticated results in fields from algebraic topology to theoretical physics, where objects have "higher structure," rely on infinite-dimensional categories in place of 1-dimensional categories, and ∞-category theory has thusfar proved unamenable to computer formalization.

View PDF Chat

Internal $\infty$-Categorical Models of Dependent Type Theory: Towards 2LTT Eating HoTT

2020-01-01

Nicolai Kraus

Using dependent type theory to formalise the syntax of dependent type theory is a very active topic of study and goes under the name of "type theory eating itself" or … Using dependent type theory to formalise the syntax of dependent type theory is a very active topic of study and goes under the name of "type theory eating itself" or "type theory in type theory." Most approaches are at least loosely based on Dybjer's categories with families (CwF's) and come with a type CON of contexts, a type family TY indexed over it modelling types, and so on. This works well in versions of type theory where the principle of unique identity proofs (UIP) holds. In homotopy type theory (HoTT) however, it is a long-standing and frequently discussed open problem whether the type theory "eats itself" and can serve as its own interpreter. The fundamental underlying difficulty seems to be that categories are not suitable to capture a type theory in the absence of UIP. In this paper, we develop a notion of $\infty$-categories with families ($\infty$-CwF's). The approach to higher categories used relies on the previously suggested semi-Segal types, with a new construction of identity substitutions that allow for both univalent and non-univalent variations. The type-theoretic universe as well as the internalised syntax are models, although it remains a conjecture that the latter is initial. To circumvent the known unsolved problem of constructing semisimplicial types, the definition is presented in two-level type theory (2LTT). Apart from introducing $\infty$-CwF's, the paper explains the shortcomings of 1-categories in type theory without UIP as well as the difficulties of and approaches to internal higher-dimensional categories.

Two-sided cartesian fibrations of synthetic $$(\infty ,1)$$-categories

2024-06-21

Jonathan Weinberger

Types Are Internal ∞-Groupoids

2021-06-29

Eric Finster , Antoine Allioux , Matthieu Sozeau

By extending type theory with a universe of definitionally associative and unital polynomial monads, we show how to arrive at a definition of opetopic type which is able to encode … By extending type theory with a universe of definitionally associative and unital polynomial monads, we show how to arrive at a definition of opetopic type which is able to encode a number of fully coherent algebraic structures. In particular, our approach leads to a definition of ∞-groupoid internal to type theory and we prove that the type of such ∞-groupoids is equivalent to the universe of types. That is, every type admits the structure of an ∞-groupoid internally, and this structure is unique.

View PDF Chat

Internal ∞-Categorical Models of Dependent Type Theory : Towards 2LTT Eating HoTT

2021-06-29

Nicolai Kraus

Using dependent type theory to formalise the syntax of dependent type theory is a very active topic of study and goes under the name of "type theory eating itself" or … Using dependent type theory to formalise the syntax of dependent type theory is a very active topic of study and goes under the name of "type theory eating itself" or "type theory in type theory." Most approaches are at least loosely based on Dybjer's categories with families (CwF's) and come with a type Con of contexts, a type family Ty indexed over it modelling types, and so on. This works well in versions of type theory where the principle of unique identity proofs (UIP) holds. In homotopy type theory (HoTT) however, it is a long-standing and frequently discussed open problem whether the type theory "eats itself" and can serve as its own interpreter. The fundamental underlying difficulty seems to be that categories are not suitable to capture a type theory in the absence of UIP. In this paper, we develop a notion of ∞-categories with families (∞-CwF's). The approach to higher categories used relies on the previously suggested semi-Segal types, with a new construction of identity substitutions that allow for both univalent and non-univalent variations. The type-theoretic universe as well as the internalised (set-level) syntax are models, although it remains a conjecture that the latter is initial. To circumvent the known unsolved problem of constructing semisimplicial types, the definition is presented in two-level type theory (2LTT). Apart from introducing ∞-CwF's, the paper explains the shortcomings of 1-categories in type theory without UIP as well as the difficulties of and approaches to internal higher-dimensional categories.

View PDF Chat

Internal sums for synthetic fibered (∞,1)-categories

2024-03-18

Jonathan Weinberger

Constructing Higher Inductive Types as Groupoid Quotients

2021-04-22

Niccolò Veltri , Niels van der Weide

In this paper, we study finitary 1-truncated higher inductive types (HITs) in homotopy type theory. We start by showing that all these types can be constructed from the groupoid quotient. … In this paper, we study finitary 1-truncated higher inductive types (HITs) in homotopy type theory. We start by showing that all these types can be constructed from the groupoid quotient. We define an internal notion of signatures for HITs, and for each signature, we construct a bicategory of algebras in 1-types and in groupoids. We continue by proving initial algebra semantics for our signatures. After that, we show that the groupoid quotient induces a biadjunction between the bicategories of algebras in 1-types and in groupoids. Then we construct a biinitial object in the bicategory of algebras in groupoids, which gives the desired algebra. From all this, we conclude that all finitary 1-truncated HITs can be constructed from the groupoid quotient. We present several examples of HITs which are definable using our notion of signature. In particular, we show that each signature gives rise to a HIT corresponding to the freely generated algebraic structure over it. We also start the development of universal algebra in 1-types. We show that the bicategory of algebras has PIE limits, i.e. products, inserters and equifiers, and we prove a version of the first isomorphism theorem for 1-types. Finally, we give an alternative characterization of the foundamental groups of some HITs, exploiting our construction of HITs via the groupoid quotient. All the results are formalized over the UniMath library of univalent mathematics in Coq.

View PDF Chat

Types are Internal $\infty$-Groupoids

2021-01-01

Antoine Allioux , Eric Finster , Matthieu Sozeau

By extending type theory with a universe of definitionally associative and unital polynomial monads, we show how to arrive at a definition of opetopic type which is able to encode … By extending type theory with a universe of definitionally associative and unital polynomial monads, we show how to arrive at a definition of opetopic type which is able to encode a number of fully coherent algebraic structures. In particular, our approach leads to a definition of $\infty$-groupoid internal to type theory and we prove that the type of such $\infty$-groupoids is equivalent to the universe of types. That is, every type admits the structure of an $\infty$-groupoid internally, and this structure is unique.

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

From Cubes to Twisted Cubes via Graph Morphisms in Type Theory

2019-02-27

Gun Pinyo , Nicolai Kraus

Cube categories are used to encode higher-dimensional categorical structures. They have recently gained significant attention in the community of homotopy type theory and univalent foundations, where types carry the structure … Cube categories are used to encode higher-dimensional categorical structures. They have recently gained significant attention in the community of homotopy type theory and univalent foundations, where types carry the structure of such higher groupoids. Bezem, Coquand, and Huber have presented a constructive model of univalence using a specific cube category, which we call the BCH category. The higher categories encoded with the BCH category have the property that all morphisms are invertible, mirroring the fact that equality is symmetric. This might not always be desirable: the field of directed type theory considers a notion of equality that is not necessarily invertible. This motivates us to suggest a category of twisted cubes which avoids built-in invertibility. Our strategy is to first develop several alternative (but equivalent) presentations of the BCH category using morphisms between suitably defined graphs. Starting from there, a minor modification allows us to define our category of twisted cubes. We prove several first results about this category, and our work suggests that twisted cubes combine properties of cubes with properties of globes and simplices (tetrahedra).

Transpension: The Right Adjoint to the Pi-type

2024-06-19

Andreas Nuyts , Dominique Devriese

Presheaf models of dependent type theory have been successfully applied to model HoTT, parametricity, and directed, guarded and nominal type theory. There has been considerable interest in internalizing aspects of … Presheaf models of dependent type theory have been successfully applied to model HoTT, parametricity, and directed, guarded and nominal type theory. There has been considerable interest in internalizing aspects of these presheaf models, either to make the resulting language more expressive, or in order to carry out further reasoning internally, allowing greater abstraction and sometimes automated verification. While the constructions of presheaf models largely follow a common pattern, approaches towards internalization do not. Throughout the literature, various internal presheaf operators ($\surd$, $\Phi/\mathsf{extent}$, $\Psi/\mathsf{Gel}$, $\mathsf{Glue}$, $\mathsf{Weld}$, $\mathsf{mill}$, the strictness axiom and locally fresh names) can be found and little is known about their relative expressivenes. Moreover, some of these require that variables whose type is a shape (representable presheaf, e.g. an interval) be used affinely. We propose a novel type former, the transpension type, which is right adjoint to universal quantification over a shape. Its structure resembles a dependent version of the suspension type in HoTT. We give general typing rules and a presheaf semantics in terms of base category functors dubbed multipliers. Structural rules for shape variables and certain aspects of the transpension type depend on characteristics of the multiplier. We demonstrate how the transpension type and the strictness axiom can be combined to implement all and improve some of the aforementioned internalization operators (without formal claim in the case of locally fresh names).

View PDF Chat

Gradualizing the Calculus of Inductive Constructions

2022-04-06

Meven Lennon-Bertrand , Kenji Maillard , Nicolas Tabareau +1 more

We investigate gradual variations on the Calculus of Inductive Construction (CIC) for swifter prototyping with imprecise types and terms. We observe, with a no-go theorem, a crucial tradeoff between graduality … We investigate gradual variations on the Calculus of Inductive Construction (CIC) for swifter prototyping with imprecise types and terms. We observe, with a no-go theorem, a crucial tradeoff between graduality and the key properties of normalization and closure of universes under dependent product that CIC enjoys. Beyond this Fire Triangle of Graduality, we explore the gradualization of CIC with three different compromises, each relaxing one edge of the Fire Triangle. We develop a parametrized presentation of Gradual CIC (GCIC) that encompasses all three variations, and develop their metatheory. We first present a bidirectional elaboration of GCIC to a dependently-typed cast calculus, CastCIC, which elucidates the interrelation between typing, conversion, and the gradual guarantees. We use a syntactic model of CastCIC to inform the design of a safe, confluent reduction, and establish, when applicable, normalization. We study the static and dynamic gradual guarantees as well as the stronger notion of graduality with embedding-projection pairs formulated by New and Ahmed, using appropriate semantic model constructions. This work informs and paves the way towards the development of malleable proof assistants and dependently-typed programming languages.

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

Comprehension categories and the semantics of type dependency

1993-01-01

Bart Jacobs

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

Homotopy Theoretic Aspects of Constructive Type Theory

2008-01-01

Michael A. Warren

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.

A type theory for synthetic ∞-categories

2017-12-22

Emily Riehl , Michael Shulman

We propose foundations for a synthetic theory of $(\infty,1)$-categories within homotopy type theory. We axiomatize a directed interval type, then define higher simplices from it and use them to probe … We propose foundations for a synthetic theory of $(\infty,1)$-categories within homotopy type theory. We axiomatize a directed interval type, then define higher simplices from it and use them to probe the internal categorical structures of arbitrary types. We define \emph{Segal types}, in which binary composites exist uniquely up to homotopy; this automatically ensures composition is coherently associative and unital at all dimensions. We define \emph{Rezk types}, in which the categorical isomorphisms are additionally equivalent to the type-theoretic identities --- a ``local univalence'' condition. And we define \emph{covariant fibrations}, which are type families varying functorially over a Segal type, and prove a ``dependent Yoneda lemma'' that can be viewed as a directed form of the usual elimination rule for identity types. We conclude by studying homotopically correct adjunctions between Segal types, and showing that for a functor between Rezk types to have an adjoint is a mere proposition. To make the bookkeeping in such proofs manageable, we use a three-layered type theory with shapes, whose contexts are extended by polytopes within directed cubes, which can be abstracted over using ``extension types'' that generalize the path-types of cubical type theory. In an appendix, we describe the motivating semantics in the Reedy model structure on bisimplicial sets, in which our Segal and Rezk types correspond to Segal spaces and complete Segal spaces.

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