Natural models of homotopy type theory

Authors

Steve Awodey

Type: Article

Publication Date: 2016-11-17

Citations: 51

DOI: https://doi.org/10.1017/s0960129516000268

View Ask PDF

Abstract

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.

Locations

Mathematical Structures in Computer Science
View
arXiv (Cornell University)
PDF
OPAL (Open@LaTrobe) (La Trobe University)
View PDF

Ask a Question About This Paper

Summary

Natural models of homotopy type theory

2014-01-01

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

Chat View PDF

Natural models of homotopy type theory

2014-06-12

Steve Awodey

Chat View PDF

A model for the homotopy theory of homotopy theory

1998-01-01

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.

Chat View PDF

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.

Models of Martin-L\"of type theory from algebraic weak factorisation systems

2019-06-04

Nicola Gambino , Marco Federico Larrea

We introduce type-theoretic algebraic weak factorisation systems and show how they give rise to homotopy-theoretic models of Martin-Lof type theory. This is done by showing that the comprehension category associated … We introduce type-theoretic algebraic weak factorisation systems and show how they give rise to homotopy-theoretic models of Martin-Lof type theory. This is done by showing that the comprehension category associated to a type-theoretic algebraic weak factorisation system satisfies the assumptions necessary to apply a right adjoint method for splitting comprehension categories. We then provide methods for constructing several examples of type-theoretic algebraic weak factorisation systems, encompassing the existing groupoid model and cubical sets models, as well as some models based on normal fibrations

Chat View PDF

Algebraic models of dependent type theory

2021-01-01

Clive Newstead

The rules governing the essentially algebraic notion of a category with families have been observed (independently) by Steve Awodey and Marcelo Fiore to precisely match those of a representable natural … The rules governing the essentially algebraic notion of a category with families have been observed (independently) by Steve Awodey and Marcelo Fiore to precisely match those of a representable natural transformation between presheaves. This provides us with a natural, functorial description of essentially algebraic objects which are used to model dependent type theory; following Steve Awodey, we call them 'natural models'. We can view natural models from several different viewpoints, of which we focus on three in this thesis. First, natural models are essentially algebraic, meaning that they can be described by specifying operations between sorts, subject to equational axioms; this allows us to assemble natural models into a category with certain beneficial properties. Second, since natural models are natural transformations between presheaves, they are morphisms in a locally cartesian closed category, meaning that they can be regarded as polynomials. Third, since natural models admit interpretations of dependent type theory, we can use them to provide a functorial semantics.

Chat View PDF

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.

Model structure on the universe in a two level type theory

2017-01-01

Simon Boulier , Nicolas Tabareau

There is an ongoing connection between type theory and homotopy theory, based on the similarity between types and the notion of homotopy types for topological spaces. This idea has been … There is an ongoing connection between type theory and homotopy theory, based on the similarity between types and the notion of homotopy types for topological spaces. This idea has been made precise by exhibiting the category cSet of cubical sets as a model of homotopy type theory. It is natural to wonder, conversely, to what extend this model can be reflected in a type theory. The homotopy structure of cSet is given by a model structure; that is, a definition of three classes of maps—fibrations, cofibrations and weak equivalences—satisfying various properties. In this article, we internalize the notion of model structure in Martin-Lof type theory with a strict equality and formalize a model structure on the category of fibrant types in a type theory with two equalities (a la Voevodsky's Homotopy Type System). This formalization is conducted in Coq, taking advantage of type class inference to emulate fibrancy. We then propose a refinement of the notion of fibrancy—justified in the cubical model—by distinguishing between degenerate and regular fibrant families. In this system, a fibrant replacement is admissible (which is an open issue in the community) and gives rise to a model structure on the universe of all types.

Chat View PDF

Categorical Homotopy Theory

2014-05-26

Emily Riehl

This book develops abstract homotopy theory from the categorical perspective with a particular focus on examples. Part I discusses two competing perspectives by which one typically first encounters homotopy (co)limits: … This book develops abstract homotopy theory from the categorical perspective with a particular focus on examples. Part I discusses two competing perspectives by which one typically first encounters homotopy (co)limits: either as derived functors definable when the appropriate diagram categories admit a compatible model structure, or through particular formulae that give the right notion in certain examples. Emily Riehl unifies these seemingly rival perspectives and demonstrates that model structures on diagram categories are irrelevant. Homotopy (co)limits are explained to be a special case of weighted (co)limits, a foundational topic in enriched category theory. In Part II, Riehl further examines this topic, separating categorical arguments from homotopical ones. Part III treats the most ubiquitous axiomatic framework for homotopy theory - Quillen's model categories. Here, Riehl simplifies familiar model categorical lemmas and definitions by focusing on weak factorization systems. Part IV introduces quasi-categories and homotopy coherence.

MODELS OF MARTIN-LÖF TYPE THEORY FROM ALGEBRAIC WEAK FACTORISATION SYSTEMS

2021-06-08

Nicola Gambino , Marco Federico Larrea

We introduce type-theoretic algebraic weak factorisation systems and show how they give rise to homotopy-theoretic models of Martin-L\"of type theory. This is done by showing that the comprehension category associated … We introduce type-theoretic algebraic weak factorisation systems and show how they give rise to homotopy-theoretic models of Martin-L\"of type theory. This is done by showing that the comprehension category associated to a type-theoretic algebraic weak factorisation system satisfies the assumptions necessary to apply a right adjoint method for splitting comprehension categories. We then provide methods for constructing several examples of type-theoretic algebraic weak factorisation systems, encompassing the existing groupoid model and cubical sets models, as well as some models based on normal fibrations

Chat View PDF

Natural Models of Homotopy Type Theory (Abstract)

2013-01-01

Steve Awodey

A Bunched Homotopy Type Theory for Synthetic Stable Homotopy Theory

2022-01-01

Mitchell Vern Riley

Homotopy type theory allows for a synthetic formulation of homotopy theory, where arguments can be checked by computer and automatically apply in many semantic settings.Modern homotopy theory makes essential use … Homotopy type theory allows for a synthetic formulation of homotopy theory, where arguments can be checked by computer and automatically apply in many semantic settings.Modern homotopy theory makes essential use of the category of spectra, the natural setting in which to investigate 'stable' phenomena: the suspension and loop space operations become inverses.One can define a version of spectra internally to type theory, but this definition can be quite difficult to work with.In particular, there is not presently a convenient way to construct and manipulate the smash product and internal hom of such spectra.This thesis describes an extension of Martin-L öf Type Theory that is suitable for working with these constructions synthetically.There is an ∞-topos of parameterised spectra, whose objects are an index space with a family of spectra over it, so standard homotopy type theory can be interpreted in this setting.To isolate the spaces (as objects with the trivial family of spectra) and the spectra (as objects with trivial indexing space), we extend type theory with a novel modality ♮ that is simultaneously a monad and a comonad.Intuitively, this modality keeps the base of an object the same but replaces the spectrum over each point with a trivial one.The system is further extended with a monoidal tensor ⊗, unit S and internal hom ⊸, which capture abstractly the constructions on spectra mentioned above.We are lead naturally to consider a 'bunched' type theory, where the contexts have a tree-like structure.The modality is crucial for making dependency in these linear type formers work correctly: dependency between ⊗ 'bunches' is mediated by ♮.To demonstrate that this type theory is usable in practice, we prove some basic synthetic results in this new system.For example, externally, any map of spaces induces a 'six-functor formalism' between the categories of parameterised spectra over those spaces, and this structure can be reconstructed internal to the type theory.We additionally investigate an axiom asserting that the internal category of spectra is semiadditive; we show that in the presence of univalence this in fact implies that the category of spectra is stable.This thesis could not have been written without the limitless type-theoretic wisdom and equally limitless patience and kindness of my advisor Dan Licata.His support made it possible to persist past the many syntactic dead ends that I walked myself down, and he has my deepest gratitude.I am grateful to the members of the HoTT community for countless enlightening conversations, particularly Eric Finster, Mike Shulman, Mathieu Anel, David Jaz Myers, and all of the HoTT MURI Team.I owe a particular debt to Eric, for putting forward what has proven to be a fruitful avenue for research.

A type theory for synthetic $\infty$-categories

2017-01-01

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 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 Rezk types, in which the categorical isomorphisms are additionally equivalent to the type-theoretic identities - a "local univalence" condition. And we define 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.

Chat View PDF

A type theory for synthetic $\infty$-categories

2017-05-21

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 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 Rezk types, in which the categorical isomorphisms are additionally equivalent to the type-theoretic identities - a local univalence condition. And we define 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 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 correspond to Segal spaces and complete Segal spaces.

Chat View PDF

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.

Chat View PDF

Axioms for Modelling Cubical Type Theory in a Topos

2016-08-25

Ian Orton , Andrew M. Pitts

The homotopical approach to intensional type theory views proofs of equality as paths. We explore what is required of an interval-like object I in a topos to give a model … The homotopical approach to intensional type theory views proofs of equality as paths. We explore what is required of an interval-like object I in a topos to give a model of type theory in which elements of identity types are functions with domain I. Cohen, Coquand, Huber and Mortberg give such a model using a particular category of presheaves. We investigate the extent to which their model construction can be expressed in the internal type theory of any topos and identify a collection of quite weak axioms for this purpose. This clarifies the definition and properties of the notion of uniform Kan filling that lies at the heart of their constructive interpretation of Voevodsky's univalence axiom. Furthermore, since our axioms can be satisfied in a number of different ways, we show that there is a range of topos-theoretic models of homotopy type theory in this style.

Chat View PDF

Algebraic Models of Dependent Type Theory

2018-08-20

Clive Newstead

It has been observed [Awo16, Fio12] that the rules governing the essentially algebraic notion of a category with families [Dyb96] precisely match those of a representable natural transformation between presheaves. … It has been observed [Awo16, Fio12] that the rules governing the essentially algebraic notion of a category with families [Dyb96] precisely match those of a representable natural transformation between presheaves. This provides us with a natural, functorial description of essentially algebraicobjects which are used to model dependent type theory—following Steve Awodey, we call them natural models.We can view natural models from several different viewpoints, of which we focus on three in this thesis. First, natural models are essentially algebraic, meaning that they can be described by specifying operations between sorts, subject to equational axioms—this allows us to assemblenatural models into a category with certain beneficial properties. Second, since natural models are natural transformations between presheaves, they are morphisms in a locally cartesian closed category, meaning that they can be regarded as polynomials [GK13]. Third, since natural models admit interpretations of dependent type theory, we can use them to provide a functorial semantics.This thesis develops the theory of natural models in three new directions by viewing them in these three ways.Natural models as essentially algebraic objects. The first development of the thesis is to bridge the gap between the presentation of natural models as models of an essentially algebraic theory, and the functorial characterisation of natural models as representable natural transformations. Wedemonstrate that the functorial characterisations of natural models and morphisms thereof align as we hope with the essentially algebraic characterisations. Natural models as polynomials. The next development is to apply the theory of polynomials in locally cartesian closed categories to natural models. In doing so, we are able to characterise theconditions under which a natural model admits certain type theoretic structure, and under which a natural transformation is representable, entirely in the internal language of a locally cartesian closed category. In particular, we prove that a natural model admits a unit type and dependentsum types if and only if it is a polynomial pseudomonad, that it admits dependent product types if and only if it is a pseudoalgebra, and we prove various facts about the full internal subcategory associated with a natural model. Natural models as models of dependent type theory. The final development of the thesis is to demonstrate their suitability as a tool for the semantics of dependent type theory. We build the term model of a particularly simple dependent type theory and prove that it satisfies the appropriate universal property, and then we proceed by describing how to turn an arbitrary natural model intoone admitting additional type theoretic structure in an algebraically free way.

Chat View PDF

Topological and simplicial models of identity types

2010-01-01

Benno van den Berg , Richard Garner

In this paper we construct new categorical models for the identity types of Martin-L\"of 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\"of 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, which has suggested that a suitable environment for the interpretation of identity types should be a category equipped with a weak factorisation 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 factorisation 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 away from 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.

Chat View PDF

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.

Models for Homotopy Theories

2018-03-02

Julia E. Bergner

An Order-Theoretic Analysis of Universe Polymorphism

2023-01-09

Kuen-Bang Hou , Carlo Angiuli , Reed Mullanix

We present a novel formulation of universe polymorphism in dependent type theory in terms of monads on the category of strict partial orders, and a novel algebraic structure, displacement algebras, … We present a novel formulation of universe polymorphism in dependent type theory in terms of monads on the category of strict partial orders, and a novel algebraic structure, displacement algebras, on top of which one can implement a generalized form of McBride’s “crude but effective stratification” scheme for lightweight universe polymorphism. We give some examples of exotic but consistent universe hierarchies, and prove that every universe hierarchy in our sense can be embedded in a displacement algebra and hence implemented via our generalization of McBride’s scheme. Many of our technical results are mechanized in Agda, and we have an OCaml library for universe levels based on displacement algebras, for use in proof assistant implementations.

Chat View PDF

Relative induction principles for type theories

2021-02-23

Rafaël Bocquet , Ambrus Kaposi , Christian Sattler

We present new induction principles for the syntax of dependent type theories, which we call relative induction principles. The result of the induction principle relative to a functor F into … We present new induction principles for the syntax of dependent type theories, which we call relative induction principles. The result of the induction principle relative to a functor F into the syntax is stable over the codomain of F. We rely on the internal language of presheaf categories. In order to combine the internal languages of multiple presheaf categories, we use Dependent Right Adjoints and Multimodal Type Theory. Categorical gluing is used to prove these induction principles, but it not visible in their statements, which involve a notion of model without context extensions. As example applications of these induction principles, we give short and boilerplate-free proofs of canonicity and normalization for some small type theories, and sketch proofs of other metatheoretic results.

Chat View PDF

The universal exponentiable arrow

2021-12-21

Taichi Uemura

We show that the essentially algebraic theory of generalized algebraic theories, regarded as a category with finite limits, has a universal exponentiable arrow in the sense that any exponentiable arrow … We show that the essentially algebraic theory of generalized algebraic theories, regarded as a category with finite limits, has a universal exponentiable arrow in the sense that any exponentiable arrow in any category with finite limits is the image of the universal exponentiable arrow by an essentially unique functor.

Chat View PDF

A Cubical Language for Bishop Sets

2022-03-29

Jonathan Sterling , Carlo Angiuli , Daniel Gratzer

We present XTT, a version of Cartesian cubical type theory specialized for Bishop sets \`a la Coquand, in which every type enjoys a definitional version of the uniqueness of identity … We present XTT, a version of Cartesian cubical type theory specialized for Bishop sets \`a la Coquand, in which every type enjoys a definitional version of the uniqueness of identity proofs. Using cubical notions, XTT reconstructs many of the ideas underlying Observational Type Theory, a version of intensional type theory that supports function extensionality. We prove the canonicity property of XTT (that every closed boolean is definitionally equal to a constant) using Artin gluing.

Chat View PDF

Algebraic models of simple type theories

2020-07-08

Nathanael Arkor , Marcelo Fiore

We develop algebraic models of simple type theories, laying out a framework that extends universal algebra to incorporate both algebraic sorting and variable binding. Examples of simple type theories include … We develop algebraic models of simple type theories, laying out a framework that extends universal algebra to incorporate both algebraic sorting and variable binding. Examples of simple type theories include the unityped and simply-typed λ-calculi, the computational λ-calculus, and predicate logic. Simple type theories are given models in presheaf categories, with structure specified by algebras of polynomial endofunctors that correspond to natural deduction rules. Initial models, which we construct, abstractly describe the syntax of simple type theories. Taking substitution structure into consideration, we further provide sound and complete semantics in structured cartesian multicategories. This development generalises Lambek's correspondence between the simply-typed λ-calculus and cartesian-closed categories, to arbitrary simple type theories.

Chat View PDF

Kripke-Joyal forcing for type theory and uniform fibrations

2021-01-01

Steve Awodey , Nicola Gambino , Sina Hazratpour

We introduce a new method for precisely relating certain kinds of algebraic structures in a presheaf category and judgements of its internal type theory. The method provides a systematic way … We introduce a new method for precisely relating certain kinds of algebraic structures in a presheaf category and judgements of its internal type theory. The method provides a systematic way to organise complex diagrammatic reasoning and generalises the well-known Kripke-Joyal forcing for logic. As an application, we prove several properties of algebraic weak factorisation systems considered in Homotopy Type Theory.

Chat View PDF

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.

Chat View PDF

A General Framework for the Semantics of Type Theory

2019-01-01

Taichi Uemura

We propose an abstract notion of a type theory to unify the semantics of various type theories including Martin-Löf type theory, two-level type theory and cubical type theory. We establish … We propose an abstract notion of a type theory to unify the semantics of various type theories including Martin-Löf type theory, two-level type theory and cubical type theory. We establish basic results in the semantics of type theory: every type theory has a bi-initial model; every model of a type theory has its internal language; the category of theories over a type theory is bi-equivalent to a full sub-2-category of the 2-category of models of the type theory.

Chat View PDF

Axioms for Modelling Cubical Type Theory in a Topos

2017-01-01

Ian Orton , Andrew M. Pitts

The homotopical approach to intensional type theory views proofs of equality as paths. We explore what is required of an object $I$ in a topos to give such a path-based … The homotopical approach to intensional type theory views proofs of equality as paths. We explore what is required of an object $I$ in a topos to give such a path-based model of type theory in which paths are just functions with domain $I$. Cohen, Coquand, Huber and M\"ortberg give such a model using a particular category of presheaves. We investigate the extent to which their model construction can be expressed in the internal type theory of any topos and identify a collection of quite weak axioms for this purpose. This clarifies the definition and properties of the notion of uniform Kan filling that lies at the heart of their constructive interpretation of Voevodsky's univalence axiom. (This paper is a revised and expanded version of a paper of the same name that appeared in the proceedings of the 25th EACSL Annual Conference on Computer Science Logic, CSL 2016.)

Chat View PDF

Univalence in Higher Category Theory

2021-01-01

Nima Rasekh

Univalence was first defined in the setting of homotopy type theory by Voevodsky, who also (along with Kapulkin and Lumsdaine) adapted it to a model categorical setting, which was subsequently … Univalence was first defined in the setting of homotopy type theory by Voevodsky, who also (along with Kapulkin and Lumsdaine) adapted it to a model categorical setting, which was subsequently generalized to locally Cartesian closed presentable $\infty$-categories by Gepner and Kock. These definitions were used to characterize various $\infty$-categories as models of type theories. We give a definition for univalent morphisms in finitely complete $\infty$-categories that generalizes the aforementioned definitions and completely focuses on the $\infty$-categorical aspects, characterizing it via representability of certain functors, which should remind the reader of concepts such as adjunctions or limits. We then prove that in a locally Cartesian closed $\infty$-category (that is not necessarily presentable) univalence of a morphism is equivalent to the completeness of a certain Segal object we construct out of the morphism, characterizing univalence via internal $\infty$-categories, which had been considered in a strict setting by Stenzel. We use these results to study the connection between univalence and elementary topos theory. We also study univalent morphisms in the category of groups, the $\infty$-category of $\infty$-categories, and pointed $\infty$-categories.

Chat View PDF

Cubical Syntax for Reflection-Free Extensional Equality

2019-01-01

Jonathan Sterling , Carlo Angiuli , Daniel Gratzer

We contribute XTT, a cubical reconstruction of Observational Type Theory which extends Martin-Löf's intensional type theory with a dependent equality type that enjoys function extensionality and a judgmental version of … We contribute XTT, a cubical reconstruction of Observational Type Theory which extends Martin-Löf's intensional type theory with a dependent equality type that enjoys function extensionality and a judgmental version of the unicity of identity types principle (UIP): any two elements of the same equality type are judgmentally equal. Moreover, we conjecture that the typing relation can be decided in a practical way. In this paper, we establish an algebraic canonicity theorem using a novel cubical extension (independently proposed by Awodey) of the logical families or categorical gluing argument inspired by Coquand and Shulman: every closed element of boolean type is derivably equal to either 'true' or 'false'.

Chat View PDF

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.

Chat View PDF

Algebraic models of simple type theories: a polynomial approach

2020-06-30

Nathanael Arkor , Marcelo Fiore

We develop algebraic models of simple type theories, laying out a framework that extends universal algebra to incorporate both algebraic sorting and variable binding. Examples of simple type theories include … We develop algebraic models of simple type theories, laying out a framework that extends universal algebra to incorporate both algebraic sorting and variable binding. Examples of simple type theories include the unityped and simply-typed $\lambda$-calculi, the computational $\lambda$-calculus, and predicate logic. Simple type theories are given models in presheaf categories, with structure specified by algebras of polynomial endofunctors that correspond to natural deduction rules. Initial models, which we construct, abstractly describe the syntax of simple type theories. Taking substitution structure into consideration, we further provide sound and complete semantics in structured cartesian multicategories. This development generalises Lambek's correspondence between the simply-typed $\lambda$-calculus and cartesian-closed categories, to arbitrary simple type theories.

Chat View PDF

Polynomial pseudomonads and dependent type theory

2018-01-01

Steve Awodey , Clive Newstead

We assemble polynomials in a locally cartesian closed category into a tricategory, allowing us to define the notion of a polynomial pseudomonad and polynomial pseudoalgebra. Working in the context of … We assemble polynomials in a locally cartesian closed category into a tricategory, allowing us to define the notion of a polynomial pseudomonad and polynomial pseudoalgebra. Working in the context of natural models of type theory, we prove that dependent type theories admitting a unit type and dependent sum types give rise to polynomial pseudomonads, and that those admitting dependent product types give rise to polynomial pseudoalgebras.

Chat View PDF

A general framework for the semantics of type theory

2023-03-01

Taichi Uemura

Abstract We propose an abstract notion of a type theory to unify the semantics of various type theories including Martin–Löf type theory, two-level type theory, and cubical type theory. We … Abstract We propose an abstract notion of a type theory to unify the semantics of various type theories including Martin–Löf type theory, two-level type theory, and cubical type theory. We establish basic results in the semantics of type theory: every type theory has a bi-initial model; every model of a type theory has its internal language; the category of theories over a type theory is bi-equivalent to a full sub-2-category of the 2-category of models of the type theory.

Chat View PDF

Partial Univalence in n-truncated Type Theory

2020-05-26

Christian Sattler , Andrea Vezzosi

Chat View PDF

Modalities and Parametric Adjoints

2022-03-29

Daniel Gratzer , Evan Cavallo , G. A. Kavvos +2 more

Birkedal et al. recently introduced dependent right adjoints as an important class of (non-fibered) modalities in type theory. We observe that several aspects of their calculus are left underdeveloped and … Birkedal et al. recently introduced dependent right adjoints as an important class of (non-fibered) modalities in type theory. We observe that several aspects of their calculus are left underdeveloped and that it cannot serve as an internal language. We resolve these problems by assuming that the modal context operator is a parametric right adjoint. We show that this hitherto unrecognized structure is common. Based on these discoveries we present a new well-behaved Fitch-style multimodal type theory, which can be used as an internal language. Finally, we apply this syntax to guarded recursion and parametricity.

Chat View PDF

Models of Type Theory Based on Moore Paths

2018-01-01

Ian Orton , Andrew M. Pitts

This paper introduces a new family of models of intensional Martin-L\"of type theory. We use constructive ordered algebra in toposes. Identity types in the models are given by a notion … This paper introduces a new family of models of intensional Martin-L\"of type theory. We use constructive ordered algebra in toposes. Identity types in the models are given by a notion of Moore path. By considering a particular gros topos, we show that there is such a model that is non-truncated, i.e. contains non-trivial structure at all dimensions. In other words, in this model a type in a nested sequence of identity types can contain more than one element, no matter how great the degree of nesting. Although inspired by existing non-truncated models of type theory based on simplicial and cubical sets, the notion of model presented here is notable for avoiding any form of Kan filling condition in the semantics of types.

Chat View PDF

Bicategories in Univalent Foundations

2019-03-04

Benedikt Ahrens , Dan Frumin , Marco Maggesi +2 more

We develop bicategory theory in univalent foundations. Guided by the notion of univalence for (1-)categories studied by Ahrens, Kapulkin, and Shulman, we define and study univalent bicategories. To construct examples … We develop bicategory theory in univalent foundations. Guided by the notion of univalence for (1-)categories studied by Ahrens, Kapulkin, and Shulman, we define and study univalent bicategories. To construct examples of univalent bicategories, we develop the notion of `displayed bicategories', an analog of displayed 1-categories introduced by Ahrens and Lumsdaine. Displayed bicategories allow us to construct univalent bicategories in a modular fashion. We demonstrate the applicability of this notion, and prove that several bicategories of interest are univalent. Among these are the bicategory of univalent categories with families and the bicategory of pseudofunctors between univalent bicategories. Furthermore, we show that every bicategory with univalent hom-category is weakly equivalent to a univalent bicategory. All of our work is formalized in Coq as part of the UniMath library of univalent mathematics.

Chat View PDF

The category of iterative sets in homotopy type theory and univalent foundations

2024-11-19

Daniel Gratzer , Håkon Robbestad Gylterud , Anders Mörtberg +1 more

Abstract When working in homotopy type theory and univalent foundations, the traditional role of the category of sets, $\mathcal{Set}$ , is replaced by the category $\mathcal{hSet}$ of homotopy sets (h-sets); … Abstract When working in homotopy type theory and univalent foundations, the traditional role of the category of sets, $\mathcal{Set}$ , is replaced by the category $\mathcal{hSet}$ of homotopy sets (h-sets); types with h-propositional identity types. Many of the properties of $\mathcal{Set}$ hold for $\mathcal{hSet}$ ((co)completeness, exactness, local cartesian closure, etc.). Notably, however, the univalence axiom implies that $\mathsf{Ob}\,\mathcal{hSet}$ is not itself an h-set, but an h-groupoid. This is expected in univalent foundations, but it is sometimes useful to also have a stricter universe of sets, for example, when constructing internal models of type theory. In this work, we equip the type of iterative sets $\mathsf{V}^0$ , due to Gylterud ((2018). The Journal of Symbolic Logic 83 (3) 1132–1146) as a refinement of the pioneering work of Aczel ((1978). Logic Colloquium’77 , Studies in Logic and the Foundations of Mathematics, vol. 96, Elsevier, 55–66.) on universes of sets in type theory, with the structure of a Tarski universe and show that it satisfies many of the good properties of h-sets. In particular, we organize $\mathsf{V}^0$ into a (non-univalent strict) category and prove that it is locally cartesian closed. This enables us to organize it into a category with families with the structure necessary to model extensional type theory internally in HoTT/UF. We do this in a rather minimal univalent type theory with W-types, in particular we do not rely on any HITs, or other complex extensions of type theory. Furthermore, the construction of $\mathsf{V}^0$ and the model is fully constructive and predicative, while still being very convenient to work with as the decoding from $\mathsf{V}^0$ into h-sets commutes definitionally for all type constructors. Almost all of the paper has been formalized in $\texttt{Agda}$ using the $\texttt{agda}$ - $\texttt{unimath}$ library of univalent mathematics.

Chat View PDF

Truncation levels in homotopy type theory

2015-07-15

Nicolai Kraus

Homotopy type theory (HoTT) is a branch of mathematics that combines and benefits from a variety of fields, most importantly homotopy theory, higher dimensional category theory, and, of course, type … Homotopy type theory (HoTT) is a branch of mathematics that combines and benefits from a variety of fields, most importantly homotopy theory, higher dimensional category theory, and, of course, type theory. We present several original results in homotopy type theory which are related to the truncation level of types, a concept due to Voevodsky. To begin, we give a few simple criteria for determining whether a type is 0-truncated (a set), inspired by a well-known theorem by Hedberg, and these criteria are then generalised to arbitrary n. This naturally leads to a discussion of functions that are weakly constant, i.e. map any two inputs to equal outputs. A weakly constant function does in general not factor through the propositional truncation of its domain, something that one could expect if the function really did not depend on its input. However, the factorisation is always possible for weakly constant endofunctions, which makes it possible to define a propositional notion of anonymous existence. We additionally find a few other non-trivial special cases in which the factorisation works. Further, we present a couple of constructions which are only possible with the judgmental computation rule for the truncation. Among these is an invertibility puzzle that seemingly inverts the canonical map from Nat to the truncation of Nat, which is perhaps surprising as the latter type is equivalent to the unit type. A further result is the construction of strict n-types in Martin-Lof type theory with a hierarchy of univalent universes (and without higher inductive types), and a proof that the universe U(n) is not n-truncated. This solves a hitherto open problem of the 2012/13 special year program on Univalent Foundations at the Institute for Advanced Study (Princeton). The main result of this thesis is a generalised universal property of the propositional truncation, using a construction of coherently constant functions. We show that the type of such coherently constant functions between types A and B, which can be seen as the type of natural transformations between two diagrams over the simplex category without degeneracies (i.e. finite non-empty sets and strictly increasing functions), is equivalent to the type of functions with the truncation of A as domain and B as codomain. In the general case, the definition of natural transformations between such diagrams requires an infinite tower of conditions, which exists if the type theory has Reedy limits of diagrams over the ordinal omega. If B is an n-type for some given finite n, (non-trivial) Reedy limits are unnecessary, allowing us to construct functions from the truncation of A to B in homotopy type theory without further assumptions. To obtain these results, we develop some theory on equality diagrams, especially equality semi-simplicial types. In particular, we show that the semi-simplicial equality type over any type satisfies the Kan condition, which can be seen as the simplicial version of the fundamental result by Lumsdaine, and by van den Berg and Garner, that types are weak omega-groupoids. Finally, we present some results related to formalisations of infinite structures that seem to be impossible to express internally. To give an example, we show how the simplex category can be implemented so that the categorical laws hold strictly. In the presence of very dependent types, we speculate that this makes the Reedy approach for the famous open problem of defining semi-simplicial types work.

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.

Chat View PDF

The Universal Exponentiable Arrow

2020-01-27

Taichi Uemura

We show that the essentially algebraic theory of a generalized algebraic theory, regarded as a category with finite limits, has a universal exponentiable arrow in the sense that any exponentiable … We show that the essentially algebraic theory of a generalized algebraic theory, regarded as a category with finite limits, has a universal exponentiable arrow in the sense that any exponentiable arrow in any category with finite limits is the image of the universal exponentiable arrow by an essentially unique functor.

Partial Univalence in n-truncated Type Theory

2020-05-01

Christian Sattler , Andrea Vezzosi

It is well known that univalence is incompatible with uniqueness of identity proofs (UIP), the axiom that all types are h-sets. This is due to finite h-sets having non-trivial automorphisms … It is well known that univalence is incompatible with uniqueness of identity proofs (UIP), the axiom that all types are h-sets. This is due to finite h-sets having non-trivial automorphisms as soon as they are not h-propositions. A natural question is then whether univalence restricted to h-propositions is compatible with UIP. We answer this affirmatively by constructing a model where types are elements of a closed universe defined as a higher inductive type in homotopy type theory. This universe has a path constructor for simultaneous partial univalent completion, i.e., restricted to h-propositions. More generally, we show that univalence restricted to $(n-1)$-types is consistent with the assumption that all types are $n$-truncated. Moreover we parametrize our construction by a suitably well-behaved container, to abstract from a concrete choice of type formers for the universe.

Chat View PDF

Algebraic Models of Dependent Type Theory

2018-08-20

Clive Newstead

Chat View PDF

Syntactic categories for dependent type theory: sketching and adequacy.

2020-12-19

Daniel Gratzer , Jonathan Sterling

We argue that locally Cartesian closed categories form a suitable doctrine for defining dependent type theories, including non-extensional ones. Using the theory of sketches, one may define syntactic categories for … We argue that locally Cartesian closed categories form a suitable doctrine for defining dependent type theories, including non-extensional ones. Using the theory of sketches, one may define syntactic categories for type theories in a style that resembles the use of Martin-Lof's Logical Framework, following the as types principle. The concentration of type theories into their locally Cartesian closed categories of judgments is particularly convenient for proving syntactic metatheorems by semantic means (canonicity, normalization, etc.). Perhaps surprisingly, the notion of a context plays no role in the definitions of type theories in this sense, but the structure of a class of display maps can be imposed on a theory post facto wherever needed, as advocated by the Edinburgh school and realized by the %worlds declarations of the Twelf proof assistant. Uemura has proposed representable map categories together with a stratified logical framework for similar purposes. The stratification in Uemura's framework restricts the use of dependent products to be strictly positive, in contrast to the tradition of Martin-Lof's logical framework and Schroeder-Heister's analysis of higher-level deductions. We prove a semantic adequacy result for locally Cartesian closed categories relative to Uemura's representable map categories: if a theory is definable in the framework of Uemura, the locally Cartesian closed category that it generates is a conservative (fully faithful) extension of its syntactic representable map category. On this basis, we argue for the use of locally Cartesian closed categories as a simpler alternative to Uemura's representable map categories.

Chat View PDF

A Cubical Language for Bishop Sets.

2020-03-03

Jonathan Sterling , Carlo Angiuli , Daniel Gratzer

We present XTT, a version of Cartesian cubical type theory specialized for Bishop sets a la Coquand, in which every type enjoys a definitional version of the uniqueness of identity … We present XTT, a version of Cartesian cubical type theory specialized for Bishop sets a la Coquand, in which every type enjoys a definitional version of the uniqueness of identity proofs. Using cubical notions, XTT reconstructs many of the ideas underlying Observational Type Theory, a version of intensional type theory that supports function extensionality. We prove the canonicity property of XTT (that every closed boolean is definitionally equal to a constant) by Artin gluing.

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.

Chat View PDF

Normalization for Cubical Type Theory

2021-01-27

Jonathan Sterling , Carlo Angiuli

We prove normalization for (univalent, Cartesian) cubical type theory, closing the last major open problem in the syntactic metatheory of cubical type theory. Our normalization result is reduction-free, in the … We prove normalization for (univalent, Cartesian) cubical type theory, closing the last major open problem in the syntactic metatheory of cubical type theory. Our normalization result is reduction-free, in the sense of yielding a bijection between equivalence classes of terms in context and a tractable language of $\beta/\eta$-normal forms. As corollaries we obtain both decidability of judgmental equality and the injectivity of type constructors.

On the ∞$\infty$‐topos semantics of homotopy type theory

2024-02-01

Emily Riehl

Abstract Many introductions to homotopy type theory and the univalence axiom gloss over the semantics of this new formal system in traditional set‐based foundations. This expository article, written as lecture … Abstract Many introductions to homotopy type theory and the univalence axiom gloss over the semantics of this new formal system in traditional set‐based foundations. This expository article, written as lecture notes to accompany a three‐part mini course delivered at the Logic and Higher Structures workshop at CIRM‐Luminy, attempt to survey the state of the art, first presenting Voevodsky's simplicial model of univalent foundations and then touring Shulman's vast generalization, which provides an interpretation of homotopy type theory with strict univalent universes in any ‐topos. As we will explain, this achievement was the product of a community effort to abstract and streamline the original arguments as well as develop new lines of reasoning.

Normalization for Cubical Type Theory

2021-06-29

Jonathan Sterling , Carlo Angiuli

We prove normalization for (univalent, Cartesian) cubical type theory, closing the last major open problem in the syntactic metatheory of cubical type theory. Our normalization result is reduction-free, in the … We prove normalization for (univalent, Cartesian) cubical type theory, closing the last major open problem in the syntactic metatheory of cubical type theory. Our normalization result is reduction-free, in the sense of yielding a bijection between equivalence classes of terms in context and a tractable language of $β/η$-normal forms. As corollaries we obtain both decidability of judgmental equality and the injectivity of type constructors.

Chat View PDF

Kripke-Joyal forcing for type theory and uniform fibrations

2024-07-31

Steve Awodey , Nicola Gambino , Sina Hazratpour

Abstract We introduce a new method for precisely relating algebraic structures in a presheaf category and judgements of its internal type theory. The method provides a systematic way to organise … Abstract We introduce a new method for precisely relating algebraic structures in a presheaf category and judgements of its internal type theory. The method provides a systematic way to organise complex diagrammatic reasoning and generalises the well-known Kripke-Joyal forcing for logic. As an application, we prove several properties of algebraic weak factorisation systems considered in Homotopy Type Theory.

Chat View PDF

Multimodal Dependent Type Theory

2020-11-30

Daniel Gratzer , G. A. Kavvos , Andreas Nuyts +1 more

We introduce MTT, a dependent type theory which supports multiple modalities. MTT is parametrized by a mode theory which specifies a collection of modes, modalities, and transformations between them. We … We introduce MTT, a dependent type theory which supports multiple modalities. MTT is parametrized by a mode theory which specifies a collection of modes, modalities, and transformations between them. We show that different choices of mode theory allow us to use the same type theory to compute and reason in many modal situations, including guarded recursion, axiomatic cohesion, and parametric quantification. We reproduce examples from prior work in guarded recursion and axiomatic cohesion -- demonstrating that MTT constitutes a simple and usable syntax whose instantiations intuitively correspond to previous handcrafted modal type theories. In some cases, instantiating MTT to a particular situation unearths a previously unknown type theory that improves upon prior systems. Finally, we investigate the metatheory of MTT. We prove the consistency of MTT and establish canonicity through an extension of recent type-theoretic gluing techniques. These results hold irrespective of the choice of mode theory, and thus apply to a wide variety of modal situations.

Chat View PDF

Temporal Type Theory: A Topos-Theoretic Approach to Systems and Behavior

2019-01-30

Patrick Schultz , David I. Spivak

This book introduces a temporal type theory, the first of its kind as far as we know. It is based on a standard core, and as such it can be … This book introduces a temporal type theory, the first of its kind as far as we know. It is based on a standard core, and as such it can be formalized in a proof assistant such as Coq or Lean by adding a number of axioms. Well-known temporal logics---such as Linear and Metric Temporal Logic (LTL and MTL)---embed within the logic of temporal type theory. The types in this theory represent behavior types. The language is rich enough to allow one to define arbitrary hybrid dynamical systems, which are mixtures of continuous dynamics---e.g. as described by a differential equation---and discrete jumps. In particular, the derivative of a continuous real-valued function is internally defined. We construct a semantics for the temporal type theory in the topos of sheaves on a translation-invariant quotient of the standard interval domain. In fact, domain theory plays a recurring role in both the semantics and the type theory.

Native Type Theory

2022-10-31

Christian Williams , Michael Stay

Native type systems are those in which type constructors are derived from term constructors, as well as the constructors of predicate logic and intuitionistic type theory. We present a method … Native type systems are those in which type constructors are derived from term constructors, as well as the constructors of predicate logic and intuitionistic type theory. We present a method to construct native type systems for a broad class of languages, lambda-theories with equality, by embedding such a theory into the internal language of its topos of presheaves. Native types provide total specification of the structure of terms; and by internalizing transition systems, native type systems serve to reason about structure and behavior simultaneously. The construction is functorial, thereby providing a shared framework of higher-order reasoning for many languages, including programming languages.

Chat View PDF

Algebraic models of simple type theories

2020-05-26

Nathanael Arkor , Marcelo Fiore

Chat View PDF

Multimodal Dependent Type Theory

2020-05-26

Daniel Gratzer , G. A. Kavvos , Andreas Nuyts +1 more

We introduce MTT, a dependent type theory which supports multiple modalities. MTT is parametrized by a mode theory which specifies a collection of modes, modalities, and transformations between them. We … We introduce MTT, a dependent type theory which supports multiple modalities. MTT is parametrized by a mode theory which specifies a collection of modes, modalities, and transformations between them. We show that different choices of mode theory allow us to use the same type theory to compute and reason in many modal situations, including guarded recursion, axiomatic cohesion, and parametric quantification. We reproduce examples from prior work in guarded recursion and axiomatic cohesion --- demonstrating that MTT constitutes a simple and usable syntax whose instantiations intuitively correspond to previous handcrafted modal type theories. In some cases, instantiating MTT to a particular situation unearths a previously unknown type theory that improves upon prior systems. Finally, we investigate the metatheory of MTT. We prove the consistency of MTT and establish canonicity through an extension of recent type-theoretic gluing techniques. These results hold irrespective of the choice of mode theory, and thus apply to a wide variety of modal situations.

Chat View PDF

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

2019-04-01

Simon Castellan , Pierre Clairambault , Peter Dybjer

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

Chat View PDF

Normalization for Multimodal Type Theory

2022-08-02

Daniel Gratzer

We prove normalization for MTT, a general multimodal dependent type theory capable of expressing modal type theories for guarded recursion, internalized parametricity, and various other prototypical modal situations. We prove … We prove normalization for MTT, a general multimodal dependent type theory capable of expressing modal type theories for guarded recursion, internalized parametricity, and various other prototypical modal situations. We prove that deciding type checking and conversion in MTT can be reduced to deciding the equality of modalities in the underlying modal situation, immediately yielding a type checking algorithm for all instantiations of MTT in the literature. This proof follows from a generalization of synthetic Tait computability—an abstract approach to gluing proofs—to account for modalities. This extension is based on MTT itself, so that this proof also constitutes a significant case study of MTT.

Chat View PDF

Multimodal Dependent Type Theory

2021-07-28

Daniel Gratzer , G. A. Kavvos , Andreas Nuyts +1 more

We introduce MTT, a dependent type theory which supports multiple modalities. MTT is parametrized by a mode theory which specifies a collection of modes, modalities, and transformations between them. We … We introduce MTT, a dependent type theory which supports multiple modalities. MTT is parametrized by a mode theory which specifies a collection of modes, modalities, and transformations between them. We show that different choices of mode theory allow us to use the same type theory to compute and reason in many modal situations, including guarded recursion, axiomatic cohesion, and parametric quantification. We reproduce examples from prior work in guarded recursion and axiomatic cohesion, thereby demonstrating that MTT constitutes a simple and usable syntax whose instantiations intuitively correspond to previous handcrafted modal type theories. In some cases, instantiating MTT to a particular situation unearths a previously unknown type theory that improves upon prior systems. Finally, we investigate the metatheory of MTT. We prove the consistency of MTT and establish canonicity through an extension of recent type-theoretic gluing techniques. These results hold irrespective of the choice of mode theory, and thus apply to a wide variety of modal situations.

Chat View PDF

Discrete Generalised Polynomial Functors

2012-01-01

Marcelo Fiore

Natural models of homotopy type theory

2014-06-12

Steve Awodey

Chat View PDF

On the interpretation of type theory in locally cartesian closed categories

1995-01-01

Martin Hofmann

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.

Chat View PDF

Exponentiable morphisms, partial products and pullback complements

1987-11-01

Roy Dyckhoff , Walter Tholen

Topological and Simplicial Models of Identity Types

2012-01-01

Benno van den Berg , Richard Garner

Chat View PDF

Variations on the bagdomain theme

1994-12-01

Peter Johnstone

Relating first-order set theories, toposes and categories of classes

2013-07-08

Steve Awodey , Carsten Butz , Alex Simpson +1 more

Chat View PDF

A model of type theory in cubical sets

2014-01-01

M Bezem , Thierry Coquand , Simon Huber

We present a model of type theory with dependent product, sum, and identity, in cubical sets. We describe a universe and explain how to transform an equivalence between two types … We present a model of type theory with dependent product, sum, and identity, in cubical sets. We describe a universe and explain how to transform an equivalence between two types into an equality. We also explain how to model propositional truncation and the circle. While not expressed internally in type theory, the model is expressed in a constructive metalogic. Thus it is a step towards a computational interpretation of Voevodsky's Univalence Axiom.

Polynomial functors and polynomial monads

2012-09-06

Nicola Gambino , Joachim Kock

We study polynomial functors over locally cartesian closed categories. After setting up the basic theory, we show how polynomial functors assemble into a double category, in fact a framed bicategory. … We study polynomial functors over locally cartesian closed categories. After setting up the basic theory, we show how polynomial functors assemble into a double category, in fact a framed bicategory. We show that the free monad on a polynomial endofunctor is polynomial. The relationship with operads and other related notions is explored.

Chat View PDF

THE SIMPLICIAL MODEL OF UNIVALENT FOUNDATIONS

2014-01-01

Krzysztof Kapulkin , Peter LeFanu Lumsdaine , Vladimir Voevodsky

In this paper, we construct and investigate a model of the Univalent Foundations of Mathematics in the category of simplicial sets. To this end, we rst give a new technique … In this paper, we construct and investigate a model of the Univalent Foundations of Mathematics in the category of simplicial sets. To this end, we rst give a new technique for constructing models of dependent type theory, using universes to obtain coherence. We then construct a (weakly) universal Kan bration, 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 Univalent Foundations are at least as consistent as ZFC with two inaccessible cardinals.

Chat View PDF

The identity type weak factorisation system

2008-09-03

Nicola Gambino , Richard Garner

Chat View PDF

Partial products, bagdomains and hyperlocal toposes

1992-06-26

Peter Johnstone

In a recent paper, Steven Vickers introduced a 'generalized powerdomain' construction, which he called the (lower) bagdomain, for algebraic posets, and argued that it provides a more realistic model than … In a recent paper, Steven Vickers introduced a 'generalized powerdomain' construction, which he called the (lower) bagdomain, for algebraic posets, and argued that it provides a more realistic model than the powerdomain for the theory of databases (cf. Gunter). The basic idea is that our 'partial information' about a possible database should be specified not by a set of partial records of individuals, but by an indexed family (or, in Vickers' terminology, a bag) of such records: we do not want to be forced to identify two individuals in our database merely because the information that we have about them so far happens to be identical (even though we may, at some later stage, obtain the information that they are in fact the same individual).

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.

Chat View PDF

The local universes model: an overlooked coherence construction for dependent type theories

2014-11-06

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.

Chat View PDF