We describe a non-extensional variant of Martin-L\"of type theory which we call two-dimensional type theory, and equip it with a sound and complete semantics valued in 2-categories.
We 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.
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.
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.
We define a general class of dependent type theories, encompassing Martin-Löf's intuitionistic type theories and variants and extensions. The primary aim is pragmatic: to unify and organise their study, allowing âŠ
We define a general class of dependent type theories, encompassing Martin-Löf's intuitionistic type theories and variants and extensions. The primary aim is pragmatic: to unify and organise their study, allowing results and constructions to be given in reasonable generality, rather than just for specific theories. Compared to other approaches, our definition stays closer to the direct or naive reading of syntax, yielding the traditional presentations of specific theories as closely as possible. Specifically, we give three main definitions: raw type theories, a minimal setup for discussing dependently typed derivability; acceptable type theories, including extra conditions ensuring well-behavedness; and well-presented type theories, generalising how in traditional presentations, the well-behavedness of a type theory is established step by step as the type theory is built up. Following these, we show that various fundamental fitness-for-purpose metatheorems hold in this generality. Much of the present work has been formalised in the proof assistant Coq.
We define and develop two-level type theory (2LTT), a version of Martin-L\"of type theory which combines two different type theories. We refer to them as the inner and the outer âŠ
We define and develop two-level type theory (2LTT), a version of Martin-L\"of type theory which combines two different type theories. We refer to them as the inner and the outer type theory. In our case of interest, the inner theory is homotopy type theory (HoTT) which may include univalent universes and higher inductive types. The outer theory is a traditional form of type theory validating uniqueness of identity proofs (UIP). One point of view on it is as internalised meta-theory of the inner type theory. There are two motivations for 2LTT. Firstly, there are certain results about HoTT which are of meta-theoretic nature, such as the statement that semisimplicial types up to level $n$ can be constructed in HoTT for any externally fixed natural number $n$. Such results cannot be expressed in HoTT itself, but they can be formalised and proved in 2LTT, where $n$ will be a variable in the outer theory. This point of view is inspired by observations about conservativity of presheaf models. Secondly, 2LTT is a framework which is suitable for formulating additional axioms that one might want to add to HoTT. This idea is heavily inspired by Voevodsky's Homotopy Type System (HTS), which constitutes one specific instance of a 2LTT. HTS has an axiom ensuring that the type of natural numbers behaves like the external natural numbers, which allows the construction of a universe of semisimplicial types. In 2LTT, this axiom can be stated simply be asking the inner and outer natural numbers to be isomorphic. After defining 2LTT, we set up a collection of tools with the goal of making 2LTT a convenient language for future developments. As a first such application, we develop the theory of Reedy fibrant diagrams in the style of Shulman. Continuing this line of thought, we suggest a definition of (infinity,1)-category and give some examples.
We define and develop two-level type theory (2LTT), a version of Martin-Löf type theory which combines two different type theories. We refer to them as the inner and the outer âŠ
We define and develop two-level type theory (2LTT), a version of Martin-Löf type theory which combines two different type theories. We refer to them as the inner and the outer type theory. In our case of interest, the inner theory is homotopy type theory (HoTT) which may include univalent universes and higher inductive types. The outer theory is a traditional form of type theory validating uniqueness of identity proofs (UIP). One point of view on it is as internalised meta-theory of the inner type theory. There are two motivations for 2LTT. Firstly, there are certain results about HoTT which are of meta-theoretic nature, such as the statement that semisimplicial types up to level $n$ can be constructed in HoTT for any externally fixed natural number $n$. Such results cannot be expressed in HoTT itself, but they can be formalised and proved in 2LTT, where $n$ will be a variable in the outer theory. This point of view is inspired by observations about conservativity of presheaf models. Secondly, 2LTT is a framework which is suitable for formulating additional axioms that one might want to add to HoTT. This idea is heavily inspired by Voevodsky's Homotopy Type System (HTS), which constitutes one specific instance of a 2LTT. HTS has an axiom ensuring that the type of natural numbers behaves like the external natural numbers, which allows the construction of a universe of semisimplicial types. In 2LTT, this axiom can be stated simply be asking the inner and outer natural numbers to be isomorphic. After defining 2LTT, we set up a collection of tools with the goal of making 2LTT a convenient language for future developments. As a first such application, we develop the theory of Reedy fibrant diagrams in the style of Shulman. Continuing this line of thought, we suggest a definition of (infinity,1)-category and give some examples.
We define and develop two-level type theory (2LTT), a version of Martin-Lof type theory which combines two different type theories. We refer to them as the inner and the outer âŠ
We define and develop two-level type theory (2LTT), a version of Martin-Lof type theory which combines two different type theories. We refer to them as the inner and the outer type theory. In our case of interest, the inner theory is homotopy type theory (HoTT) which may include univalent universes and higher inductive types. The outer theory is a traditional form of type theory validating uniqueness of identity proofs (UIP). One point of view on it is as internalised meta-theory of the inner type theory.
There are two motivations for 2LTT. Firstly, there are certain results about HoTT which are of meta-theoretic nature, such as the statement that semisimplicial types up to level $n$ can be constructed in HoTT for any externally fixed natural number $n$. Such results cannot be expressed in HoTT itself, but they can be formalised and proved in 2LTT, where $n$ will be a variable in the outer theory. This point of view is inspired by observations about conservativity of presheaf models.
Secondly, 2LTT is a framework which is suitable for formulating additional axioms that one might want to add to HoTT. This idea is heavily inspired by Voevodsky's Homotopy Type System (HTS), which constitutes one specific instance of a 2LTT. HTS has an axiom ensuring that the type of natural numbers behaves like the external natural numbers, which allows the construction of a universe of semisimplicial types. In 2LTT, this axiom can be stated simply be asking the inner and outer natural numbers to be isomorphic.
After defining 2LTT, we set up a collection of tools with the goal of making 2LTT a convenient language for future developments. As a first such application, we develop the theory of Reedy fibrant diagrams in the style of Shulman. Continuing this line of thought, we suggest a definition of (infinity,1)-category and give some examples.
This thesis introduces the idea of two-level type theory, an extension of Martin-Löf type theory that adds a notion of strict equality as an internal primitive. A type theory with âŠ
This thesis introduces the idea of two-level type theory, an extension of Martin-Löf type theory that adds a notion of strict equality as an internal primitive. A type theory with a strict equality alongside the more conventional form of equality, the latter being of fundamental importance for the recent innovation of homotopy type theory (HoTT), was first proposed by Voevodsky, and is usually referred to as HTS. Here, we generalise and expand this idea, by developing a semantic framework that gives a systematic account of type formers for two-level systems, and proving a conservativity result relating back to a conventional type theory like HoTT. Finally, we show how a two-level theory can be used to provide partial solutions to open problems in HoTT. In particular, we use it to construct semi-simplicial types, and lay out the foundations of an internal theory of $(\infty, 1)$-categories.
This is the second in a series of papers extending Martin-Löf's meaning explanation of dependent type theory to account for higher-dimensional types. We build on the cubical realizability framework for âŠ
This is the second in a series of papers extending Martin-Löf's meaning explanation of dependent type theory to account for higher-dimensional types. We build on the cubical realizability framework for simple types developed in Part I, and extend it to a meaning explanation of dependent higher-dimensional type theory. This extension requires generalizing the computational Kan condition given in Part I, and considering the action of type families on paths. We define identification types, which classify identifications (paths) in a type, and dependent function and pair types. The main result is a canonicity theorem, which states that a closed term of boolean type evaluates to either true or false. This result establishes the first computational interpretation of higher dependent type theory by giving a deterministic operational semantics for its programs, including operations that realize the Kan condition.
We present a generalization of cartesian closed categories (CCCs) for dependent types, called dependent cartesian closed categories (DCCCs), which also provides a reformulation of categories with families (CwFs), an abstract âŠ
We present a generalization of cartesian closed categories (CCCs) for dependent types, called dependent cartesian closed categories (DCCCs), which also provides a reformulation of categories with families (CwFs), an abstract semantics for Martin-L\{o}f type theory (MLTT) which is very close to the syntax. Thus, DCCCs accomplish mathematical elegance as well as a direct interpretation of the syntax. Moreover, they capture the categorical counterpart of the generalization of the simply-typed lambda-calculus (STLC) to MLTT in syntax, and give a systematic perspective on the relation between categorical semantics for these type theories. Furthermore, we construct a term model from the syntax, establishing the completeness of our interpretation of MLTT in DCCCs.
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.
Abstract We construct a 2-equivalence $$\mathfrak {CohTheory}^{op }\simeq \mathfrak {TypeSpaceFunc}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:msup> <mml:mrow> <mml:mi>CohTheory</mml:mi> </mml:mrow> <mml:mrow> <mml:mi>op</mml:mi> </mml:mrow> </mml:msup> <mml:mo>â</mml:mo> <mml:mi>TypeSpaceFunc</mml:mi> </mml:mrow> </mml:math> . Here $$\mathfrak {CohTheory}$$ <mml:math âŠ
Abstract We construct a 2-equivalence $$\mathfrak {CohTheory}^{op }\simeq \mathfrak {TypeSpaceFunc}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:msup> <mml:mrow> <mml:mi>CohTheory</mml:mi> </mml:mrow> <mml:mrow> <mml:mi>op</mml:mi> </mml:mrow> </mml:msup> <mml:mo>â</mml:mo> <mml:mi>TypeSpaceFunc</mml:mi> </mml:mrow> </mml:math> . Here $$\mathfrak {CohTheory}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>CohTheory</mml:mi> </mml:math> is the 2-category of positive theories and $$\mathfrak {TypeSpaceFunc}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>TypeSpaceFunc</mml:mi> </mml:math> is the 2-category of type space functors. We give a precise definition of interpretations for positive logic, which will be the 1-cells in $$\mathfrak {CohTheory}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>CohTheory</mml:mi> </mml:math> . The 2-cells are definable homomorphisms. The 2-equivalence restricts to a duality of categories, making precise the philosophy that a theory is âthe sameâ as the collection of its type spaces (i.e. its type space functor). In characterising those functors that arise as type space functors, we find that they are specific instances of (coherent) hyperdoctrines. This connects two different schools of thought on the logical structure of a theory. The key ingredient, the Deligne completeness theorem, arises from topos theory, where positive theories have been studied under the name of coherent theories.
We construct a 2-equivalence $\mathfrak{CohTheory}^\text{op} \simeq \mathfrak{TypeSpaceFunc}$. Here $\mathfrak{CohTheory}$ is the 2-category of positive theories and $\mathfrak{TypeSpaceFunc}$ is the 2-category of type space functors. We give a precise definition of âŠ
We construct a 2-equivalence $\mathfrak{CohTheory}^\text{op} \simeq \mathfrak{TypeSpaceFunc}$. Here $\mathfrak{CohTheory}$ is the 2-category of positive theories and $\mathfrak{TypeSpaceFunc}$ is the 2-category of type space functors. We give a precise definition of interpretations for positive logic, which will be the 1-cells in $\mathfrak{CohTheory}$. The 2-cells are definable homomorphisms. The 2-equivalence restricts to a duality of categories, making precise the philosophy that a theory is `the same' as the collection of its type spaces (i.e. its type space functor).
In characterising those functors that arise as type space functors, we find that they are specific instances of (coherent) hyperdoctrines. This connects two different schools of thought on the logical structure of a theory.
The key ingredient, the Deligne completeness theorem, arises from topos theory, where positive theories have been studied under the name of coherent theories.
A summary is not available for this content so a preview has been provided. Please use the Get access link above for information on how to access this content.
A summary is not available for this content so a preview has been provided. Please use the Get access link above for information on how to access this content.
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.
We show that for any type in Martin-L\"of Intensional Type Theory, the terms of that type and its higher identity types form a weak omega-category in the sense of Leinster. âŠ
We show that for any type in Martin-L\"of Intensional Type Theory, the terms of that type and its higher identity types form a weak omega-category in the sense of Leinster. Precisely, we construct a contractible globular operad of definable composition laws, and give an action of this operad on the terms of any type and its identity types.
Homotopy Type Theory is a new field of mathematics based on the recently-discovered correspondence between Martin-Löf's constructive type theory and abstract homotopy theory. We have a powerful interplay between these âŠ
Homotopy Type Theory is a new field of mathematics based on the recently-discovered correspondence between Martin-Löf's constructive type theory and abstract homotopy theory. We have a powerful interplay between these disciplines - we can use geometric intuition to formulate new concepts in type theory and, conversely, use type-theoretic machinery to verify and often simplify existing mathematical proofs.
In this thesis I lift the Curry--Howard--Lambek correspondence between the simply-typed lambda calculus and cartesian closed categories to the bicategorical setting, then use the resulting type theory to prove a âŠ
In this thesis I lift the Curry--Howard--Lambek correspondence between the simply-typed lambda calculus and cartesian closed categories to the bicategorical setting, then use the resulting type theory to prove a coherence result for cartesian closed bicategories. Cartesian closed bicategories---2-categories `up to isomorphism' equipped with similarly weak products and exponentials---arise in logic, categorical algebra, and game semantics. I show that there is at most one 2-cell between any parallel pair of 1-cells in the free cartesian closed bicategory on a set and hence---in terms of the difficulty of calculating---bring the data of cartesian closed bicategories down to the familiar level of cartesian closed categories.
In fact, I prove this result in two ways. The first argument is closely related to Power's coherence theorem for bicategories with flexible bilimits. For the second, which is the central preoccupation of this thesis, the proof strategy has two parts: the construction of a type theory, and the proof that it satisfies a form of normalisation I call local coherence. I synthesise the type theory from algebraic principles using a novel generalisation of the (multisorted) abstract clones of universal algebra, called biclones. Using a bicategorical treatment of M. Fiore's categorical analysis of normalisation-by-evaluation, I then prove a normalisation result which entails the coherence theorem for cartesian closed bicategories. In contrast to previous coherence results for bicategories, the argument does not rely on the theory of rewriting or strictify using the Yoneda embedding. Along the way I prove bicategorical generalisations of a series of well-established category-theoretic results, present a notion of glueing of bicategories, and bicategorify the folklore result providing sufficient conditions for a glueing category to be cartesian closed.
Polynomial functors (over Set or other locally cartesian closed categories) are useful in the theory of data types, where they are often called containers. They are also useful in algebra, âŠ
Polynomial functors (over Set or other locally cartesian closed categories) are useful in the theory of data types, where they are often called containers. They are also useful in algebra, combinatorics, topology, and higher category theory, and in this broader perspective the polynomial aspect is often prominent and justifies the terminology. For example, Tambara's theorem states that the category of finite polynomial functors is the Lawvere theory for commutative semirings [D. Tambara, On multiplicative transfer, Comm. Alg. 21 (1993), pp. 1393â1420], [N. Gambino and J. Kock, Polynomial functors and polynomial monads, to appear in Math. Proc. Cambridge Philos. Soc., arXiv:0906.4931]. In this talk I will explain how an upgrade of the theory from sets to groupoids (or other locally cartesian closed 2-categories) is useful to deal with data types with symmetries, and provides a common generalisation of and a clean unifying framework for quotient containers (in the sense of Abbott et al.), species and analytic functors (Joyal 1985), as well as the stuff types of Baez and Dolan. The multi-variate setting also includes relations and spans, multispans, and stuff operators. An attractive feature of this theory is that with the correct homotopical approach â homotopy slices, homotopy pullbacks, homotopy colimits, etc. â the groupoid case looks exactly like the set case. After some standard examples, I will illustrate the notion of data-types-with-symmetries with examples from perturbative quantum field theory, where the symmetries of complicated tree structures of graphs play a crucial role, and can be handled elegantly using polynomial functors over groupoids. (These examples, although beyond species, are purely combinatorial and can be appreciated without background in quantum field theory.) Locally cartesian closed 2-categories provide semantics for a 2-truncated version of Martin-Löf intensional type theory. For a fullfledged type theory, locally cartesian closed â-categories seem to be needed. The theory of these is being developed by David Gepner and the author as a setting for homotopical species, and several of the results exposed in this talk are just truncations of â-results obtained in joint work with Gepner. Details will appear elsewhere.
Revisiting a classic result from M. Hofmann's dissertation, we give a direct proof of Morita equivalence, in the sense of V. Isaev, between extensional type theory and intensional type theory âŠ
Revisiting a classic result from M. Hofmann's dissertation, we give a direct proof of Morita equivalence, in the sense of V. Isaev, between extensional type theory and intensional type theory extended by the principles of functional extensionality and of uniqueness of identity proofs.
Recently Riehl and Verity have introduced â-cosmoi, which are certain simplicially enriched categories with additional structure. In this paper we investigate those â-cosmoi which are in fact 2-categories; we shall âŠ
Recently Riehl and Verity have introduced â-cosmoi, which are certain simplicially enriched categories with additional structure. In this paper we investigate those â-cosmoi which are in fact 2-categories; we shall refer to these as 2-cosmoi. We show that each 2-category with flexible limits gives rise to a 2-cosmos whose distinguished class of isofibrations consists of the normal isofibrations. Many examples arise in this way, and we show that such 2-cosmoi are minimal as Cauchy-complete 2-cosmoi. Finally, we investigate accessible 2-cosmoi and develop a few aspects of their basic theory.
Gambino and Garner proved that the syntactic category of a dependent type theory with identity types can be endowed with a weak factorization system structure, called identity type weak factorization âŠ
Gambino and Garner proved that the syntactic category of a dependent type theory with identity types can be endowed with a weak factorization system structure, called identity type weak factorization system. In this paper we consider an enrichment of Joyal's notion of tribe, which we call a tribe with weakly stable path objects, and prove a purely category-theoretic version of the identity type weak factorization system, thus generalizing Gambino and Garner's result. We conclude showing that this structure subsumes also the weak factorization systems coming from the topological and simplicial models of identity types obtained by van den Berg and Garner.
The groupoid interpretation of dependent type theory given by Hofmann and Streicher associates to each closed type a category whose objects represent the elements of that type and whose maps âŠ
The groupoid interpretation of dependent type theory given by Hofmann and Streicher associates to each closed type a category whose objects represent the elements of that type and whose maps represent proofs of equality of elements. The categorial structure ensures that equality is reflexive (identity maps) and transitive (closure under composition); the groupoid structure, which demands that every map be invertible, ensures symmetry. Families of types are interpreted as functors; the action on maps (equality proofs) ensures that families respect equality of elements of the index type. The functorial action of a type family is computationally non-trivial in the case that the groupoid associated to the index type is non-trivial. For example, one may identity elements of a universe of sets up to isomorphism, in which case the action of a family of types indexed by sets must respect set isomorphism. The groupoid interpretation is 2-dimensional in that the coherence requirements on proofs of equality are required to hold âon the noseâ, rather than up to higher dimensional equivalences. Recent work by Awodey and Lumsdaine, Voevodsky, and others extends the groupoid interpretation to higher dimensions, exposing close correspondences between type theory, higher-dimensional category theory, and homotopy theory. In this paper we consider another generalization of the groupoid interpretation that relaxes the symmetry requirement on proofs of âequivalenceâ to obtain a directed notion of transformation between elements of a type. Closed types may then be interpreted as categories, and families as functors that extend transformations on indices to transformations between families. Relaxing symmetry requires a reformulation of type theory to make the variances of type families explicit. The types themselves must be reinterpreted to take account of variance; for example, a type is contravariant in its domain, but covariant in its range. Whereas in symmetric type theory proofs of equivalence can be internalized using the Martin-Lof identity type, in directed type theory the two-dimensional structure must be made explicit at the judgemental level. The resulting 2-dimensional directed dependent type theory, or 2DTT, is validated by an interpretation into the strict 2-categoryCat of categories, functors, and natural transformations, generalizing the groupoid interpretation. We conjecture that 2DTT can be given semantics in a broad class of 2-categories, and can be extended to make the higher dimensional structure explicit. We illustrate the use of 2DTT for writing dependently typed programs over representations of syntax and logical systems.
Hofmann and Streicher showed that there is a model of the intensional form of Martin-Lofâs type theory obtained by interpreting closed types as groupoids. We show that there is also âŠ
Hofmann and Streicher showed that there is a model of the intensional form of Martin-Lofâs type theory obtained by interpreting closed types as groupoids. We show that there is also a model when closed types are interpreted as strict Ï-groupoids. The nonderivability of various truncation and uniqueness principles in intensional type theory is then an immediate consequence. In the process of constructing the interpretation we develop some Ï-categorical machinery including a version of the Grothendieck construction for strict Ï-categories.
We study the coherence and conservativity of extensions of dependent type theories by additional strict equalities. By considering notions of congruences and quotients of models of type theory, we reconstruct âŠ
We study the coherence and conservativity of extensions of dependent type theories by additional strict equalities. By considering notions of congruences and quotients of models of type theory, we reconstruct Hofmann's proof of the conservativity of Extensional Type Theory over Intensional Type Theory. We generalize these methods to type theories without the Uniqueness of Identity Proofs principle, such as variants of Homotopy Type Theory, by introducing a notion of higher congruence over models of type theory. Our definition of higher congruence is inspired by Brunerie's type-theoretic definition of weak $\infty$-groupoid. For a large class of type theories, we reduce the problem of the conservativity of equational extensions to more tractable acyclicity conditions.
Joyal's Conjecture asserts, in a mathematically precise way, that Martin--Lof dependent type theory gives rise to locally cartesian closed quasicategories. We prove this conjecture.
Joyal's Conjecture asserts, in a mathematically precise way, that Martin--Lof dependent type theory gives rise to locally cartesian closed quasicategories. We prove this conjecture.
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.
We define a notion of weak Ï-category internal to a model of Martin-Löf's type theory, and prove that each type bears a canonical weak Ï-category structure obtained from the tower âŠ
We define a notion of weak Ï-category internal to a model of Martin-Löf's type theory, and prove that each type bears a canonical weak Ï-category structure obtained from the tower of iterated identity types over that type. We show that the Ï-categories arising in this way are in fact Ï-groupoids.
Categorical structures and their pseudomaps rarely form locally presentable 2-categories in the sense of Cat-enriched category theory. However, we show that if the categorical structure in question is sufficiently weak âŠ
Categorical structures and their pseudomaps rarely form locally presentable 2-categories in the sense of Cat-enriched category theory. However, we show that if the categorical structure in question is sufficiently weak (such as the structure of monoidal, but not strict monoidal, categories) then the 2-category in question is accessible. Furthermore, we explore the flexible limits that such 2-categories possess and their interaction with filtered colimits.
We define and develop the infrastructure of homotopical inverse diagrams in categories with attributes. Specifically, given a category with attributes $C$ and an ordered homotopical inverse category $I$, we construct âŠ
We define and develop the infrastructure of homotopical inverse diagrams in categories with attributes.
Specifically, given a category with attributes $C$ and an ordered homotopical inverse category $I$, we construct the category with attributes $C^I$ of homotopical diagrams of shape $I$ in $C$ and Reedy types over these; and we show how various logical structure ($\Pi$-types, identity types, and so on) lifts from $C$ to $C^I$. This may be seen as providing a general class of diagram models of type theory.
In a companion paper The homotopy theory of type theories (arXiv:1610.00037), we apply the present results to construct semi-model structures on categories of contextual categories.
We construct a left semi-model structure on the category of intensional type theories (precisely, on $\mathrm{CxlCat_{Id,1,\Sigma(,\Pi_{ext})}}$). This presents an $\infty$-category of such type theories; we show moreover that there is âŠ
We construct a left semi-model structure on the category of intensional type theories (precisely, on $\mathrm{CxlCat_{Id,1,\Sigma(,\Pi_{ext})}}$). This presents an $\infty$-category of such type theories; we show moreover that there is an $\infty$-functor $\mathrm{Cl}_\infty$ from there to the $\infty$-category of suitably structured quasi-categories.
This allows a precise formulation of the conjectures that intensional type theory gives internal languages for higher categories, and provides a framework and toolbox for further progress on these conjectures.
The purpose of this survey article is to introduce the reader to a connection between Logic, Geometry, and Algebra which has recently come to light in the form of an âŠ
The purpose of this survey article is to introduce the reader to a connection between Logic, Geometry, and Algebra which has recently come to light in the form of an interpretation of the constructive type theory of Martin-Löf into homotopy theory, resulting in new examples of higher-dimensional categories.
Homotopy Type Theory is a new field of mathematics based on the recently-discovered correspondence between Martin-Löf's constructive type theory and abstract homotopy theory. We have a powerful interplay between these âŠ
Homotopy Type Theory is a new field of mathematics based on the recently-discovered correspondence between Martin-Löf's constructive type theory and abstract homotopy theory. We have a powerful interplay between these disciplines - we can use geometric intuition to formulate new concepts in type theory and, conversely, use type-theoretic machinery to verify and often simplify existing mathematical proofs. Higher inductive types form a crucial part of this new system since they allow us to represent mathematical objects, such as spheres, tori, pushouts, and quotients, in the type theory. We investigate a class of higher inductive types called W-suspensions which generalize Martin-Löf's well-founded trees. We show that a propositional variant of W-suspensions, whose computational behavior is determined up to a higher path, is characterized by the universal property of being a homotopy-initial algebra. As a corollary we get that W-suspensions in the strict form are homotopy-initial.
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.
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.
Recent work on homotopy type theory exploits an exciting new correspondence between Martin-Lof's dependent type theory and the mathematical disciplines of category theory and homotopy theory. The mathematics suggests new âŠ
Recent work on homotopy type theory exploits an exciting new correspondence between Martin-Lof's dependent type theory and the mathematical disciplines of category theory and homotopy theory. The mathematics suggests new principles to add to type theory, while the type theory can be used in novel ways to do computer-checked proofs in a proof assistant. In this paper, we formalize a basic result in algebraic topology, that the fundamental group of the circle is the integers. Our proof illustrates the new features of homotopy type theory, such as higher inductive types and Voevodsky's univalence axiom. It also introduces a new method for calculating the path space of a type, which has proved useful in many other examples.
Polynomial functors are useful in the theory of data types, where they are often called containers. They are also useful in algebra, combinatorics, topology, and higher category theory, and in âŠ
Polynomial functors are useful in the theory of data types, where they are often called containers. They are also useful in algebra, combinatorics, topology, and higher category theory, and in this broader perspective the polynomial aspect is often prominent and justifies the terminology. For example, Tambara's theorem states that the category of finite polynomial functors is the Lawvere theory for commutative semirings. In this talk I will explain how an upgrade of the theory from sets to groupoids is useful to deal with data types with symmetries, and provides a common generalisation of and a clean unifying framework for quotient containers (cf. Abbott et al.), species and analytic functors (Joyal 1985), as well as the stuff types of Baez-Dolan. The multi-variate setting also includes relations and spans, multispans, and stuff operators. An attractive feature of this theory is that with the correct homotopical approach - homotopy slices, homotopy pullbacks, homotopy colimits, etc. - the groupoid case looks exactly like the set case. After some standard examples, I will illustrate the notion of data-types-with-symmetries with examples from quantum field theory, where the symmetries of complicated tree structures of graphs play a crucial role, and can be handled elegantly using polynomial functors over groupoids. (These examples, although beyond species, are purely combinatorial and can be appreciated without background in quantum field theory.) Locally cartesian closed 2-categories provide semantics for 2-truncated intensional type theory. For a fullfledged type theory, locally cartesian closed \infty-categories seem to be needed. The theory of these is being developed by D.Gepner and the author as a setting for homotopical species, and several of the results exposed in this talk are just truncations of \infty-results obtained in joint work with Gepner. Details will appear elsewhere.
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.
We prove that the homotopy theory of Joyal's tribes is equivalent to that of fibration categories. As a consequence, we deduce a variant of the conjecture asserting that Martin-Lof Type âŠ
We prove that the homotopy theory of Joyal's tribes is equivalent to that of fibration categories. As a consequence, we deduce a variant of the conjecture asserting that Martin-Lof Type Theory with dependent sums and intensional identity types is the internal language of $(\infty, 1)$-categories with finite limits.
Homotopy Type Theory is a new field of mathematics based on the surprising and elegant correspondence between Martin-Lofs constructive type theory and abstract homotopy theory. We have a powerful interplay âŠ
Homotopy Type Theory is a new field of mathematics based on the surprising and elegant correspondence between Martin-Lofs constructive type theory and abstract homotopy theory. We have a powerful interplay between these disciplines - we can use geometric intuition to formulate new concepts in type theory and, conversely, use type-theoretic machinery to verify and often simplify existing mathematical proofs. A crucial ingredient in this new system are higher inductive types, which allow us to represent objects such as spheres, tori, pushouts, and quotients. We investigate a variant of higher inductive types whose computational behavior is determined up to a higher path. We show that in this setting, higher inductive types are characterized by the universal property of being a homotopy-initial algebra.
In this paper we define Martin-Lof complexes to be algebras for monads on the category of (reflexive) globular sets which freely add cells in accordance with the rules of intensional âŠ
In this paper we define Martin-Lof complexes to be algebras for monads on the category of (reflexive) globular sets which freely add cells in accordance with the rules of intensional Martin-Lof type theory. We then study the resulting categories of algebras for several theories. Our principal result is that there exists a cofibrantly generated Quillen model structure on the category of 1-truncated Martin-Lof complexes and that this category is Quillen equivalent to the category of groupoids. In particular, 1-truncated Martin-Lof complexes are a model of homotopy 1-types.
Higher inductive-inductive types (HIITs) generalize inductive types of dependent type theories in two ways. On the one hand they allow the simultaneous definition of multiple sorts that can be indexed âŠ
Higher inductive-inductive types (HIITs) generalize inductive types of dependent type theories in two ways. On the one hand they allow the simultaneous definition of multiple sorts that can be indexed over each other. On the other hand they support equality constructors, thus generalizing higher inductive types of homotopy type theory. Examples that make use of both features are the Cauchy real numbers and the well-typed syntax of type theory where conversion rules are given as equality constructors. In this paper we propose a general definition of HIITs using a small type theory, named the theory of signatures. A context in this theory encodes a HIIT by listing the constructors. We also compute notions of induction and recursion for HIITs, by using variants of syntactic logical relation translations. Building full categorical semantics and constructing initial algebras is left for future work. The theory of HIIT signatures was formalised in Agda together with the syntactic translations. We also provide a Haskell implementation, which takes signatures as input and outputs translation results as valid Agda code.
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.
Received by the editors 2004-10-30. Transmitted by Steve Lack, Ross Street and RJ Wood. Reprint published on 2005-04-23. Several typographical errors corrected 2012-05-13. 2000 Mathematics Subject Classification: 18-02, 18D10, 18D20.
Received by the editors 2004-10-30. Transmitted by Steve Lack, Ross Street and RJ Wood. Reprint published on 2005-04-23. Several typographical errors corrected 2012-05-13. 2000 Mathematics Subject Classification: 18-02, 18D10, 18D20.
With a view to further applications, we give a self-contained account of indexed limits for 2-categories, including necessary and sufficient conditions for 2-categorical completeness. Many important 2-categories fail to be âŠ
With a view to further applications, we give a self-contained account of indexed limits for 2-categories, including necessary and sufficient conditions for 2-categorical completeness. Many important 2-categories fail to be complete but do admit a wide class of limits. Accordingly, we introduce a variety of particular 2-categorical limits of practical importance, and show that certain of these suffice for the existence of indexed lax- and pseudo-limits. Other important 2-categories fail to admit even pseudo-limits, but do admit the weaker bilimits; we end by discussing these.
It is well known that for much of the mathematics of topos theory, it is in fact sufficient to use a category C whose slice categories C/ A are cartesian âŠ
It is well known that for much of the mathematics of topos theory, it is in fact sufficient to use a category C whose slice categories C/ A are cartesian closed. In such a category, the notion of a âgeneralized setâ, for example an â A -indexed setâ, is represented by a morphism B â A of C, i.e. by an object of C/ A . The point about such a category C is that C is a C-indexed category, and more, is a hyper-doctrine, so that it has a full first order logic associated with it. This logic has some peculiar aspects. For instance, the types are the objects of C and the terms are the morphisms of C. For a given type A , the predicates with a free variable of type A are morphisms into A , and âproofsâ are morphisms over A . We see here a certain âambiguityâ between the notions of type, predicate, and term, of object and proof: a term of type A is a morphism into A , which is a predicate over A ; a morphism 1 â A can be viewed either as an object of type A or as a proof of the proposition A .
Abstract We study homotopy limits for 2-categories using the theory of Quillen model categories. In order to do so, we establish the existence of projective and injective model structures on âŠ
Abstract We study homotopy limits for 2-categories using the theory of Quillen model categories. In order to do so, we establish the existence of projective and injective model structures on diagram 2-categories. Using these results, we describe the homotopical behaviour not only of conical limits but also of weighted limits. Finally, pseudo-limits are related to homotopy limits.
By Paul Taylor: 572 pp., ÂŁ50.00 (US$80.00) isbn 0 521 63107 6 (Cambridge University Press, 1999).
By Paul Taylor: 572 pp., ÂŁ50.00 (US$80.00) isbn 0 521 63107 6 (Cambridge University Press, 1999).
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.