Homotopy type theory is a new branch of mathematics, based on a recently discovered connection between homotopy theory and type theory, which brings new ideas into the very foundation of …
Homotopy type theory is a new branch of mathematics, based on a recently discovered connection between homotopy theory and type theory, which brings new ideas into the very foundation of mathematics. On the one hand, Voevodsky's subtle and beautiful "univalence axiom" implies that isomorphic structures can be identified. On the other hand, "higher inductive types" provide direct, logical descriptions of some of the basic spaces and constructions of homotopy theory. Both are impossible to capture directly in classical set-theoretic foundations, but when combined in homotopy type theory, they permit an entirely new kind of "logic of homotopy types". This suggests a new conception of foundations of mathematics, with intrinsic homotopical content, an "invariant" conception of the objects of mathematics -- and convenient machine implementations, which can serve as a practical aid to the working mathematician. This book is intended as a first systematic exposition of the basics of the resulting "Univalent Foundations" program, and a collection of examples of this new style of reasoning -- but without requiring the reader to know or learn any formal logic, or to use any computer proof assistant.
Seely's paper "Locally cartesian closed categories and type theory" contains a well-known result in categorical type theory: that the category of locally cartesian closed categories is equivalent to the category …
Seely's paper "Locally cartesian closed categories and type theory" contains a well-known result in categorical type theory: that the category of locally cartesian closed categories is equivalent to the category of Martin-L\"of type theories with Pi-types, Sigma-types and extensional identity types. However, Seely's proof relies on the problematic assumption that substitution in types can be interpreted by pullbacks. Here we prove a corrected version of Seely's theorem: that the B\'enabou-Hofmann interpretation of Martin-L\"of type theory in locally cartesian closed categories yields a biequivalence of 2-categories. To facilitate the technical development we employ categories with families as a substitute for syntactic Martin-L\"of type theories. As a second result we prove that if we remove Pi-types the resulting categories with families are biequivalent to left exact categories.
We show how to solve the word problem for simply typed λβη-calculus by using a few well-known facts about categories of presheaves and the Yoneda embedding. The formal setting for …
We show how to solve the word problem for simply typed λβη-calculus by using a few well-known facts about categories of presheaves and the Yoneda embedding. The formal setting for these results is [Pscr ]-category theory, a version of ordinary category theory where each hom-set is equipped with a partial equivalence relation. The part of [Pscr ]-category theory we develop here is constructive and thus permits extraction of programs from proofs. It is important to stress that in our method we make no use of traditional proof-theoretic or rewriting techniques. To show the robustness of our method, we give an extended treatment for more general λ-theories in the Appendix.
A higher inductive type of level 1 (a 1-hit) has constructors for points and paths only, whereas a higher inductive type of level 2 (a 2-hit) has constructors for surfaces …
A higher inductive type of level 1 (a 1-hit) has constructors for points and paths only, whereas a higher inductive type of level 2 (a 2-hit) has constructors for surfaces too. We restrict attention to finitary higher inductive types and present general schemata for the types of their point, path, and surface constructors. We also derive the elimination and equality rules from the types of constructors for 1-hits and 2-hits. Moreover, we construct a groupoid model for dependent type theory with 2-hits and point out that we obtain a setoid model for dependent type theory with 1-hits by truncating the groupoid model.
We present an algorithm for computing normal terms and types in Martin-Löf type theory with one universe and eta-conversion. We prove that two terms or types are equal in the …
We present an algorithm for computing normal terms and types in Martin-Löf type theory with one universe and eta-conversion. We prove that two terms or types are equal in the theory iff the normal forms are identical (as de Bruijn terms). It thus follows that our algorithm can be used for deciding equality in Martin-Löf type theory. The algorithm uses the technique of normalization by evaluation; normal forms are computed by first evaluating terms and types in a suitable model. The normal forms are then extracted from the semantic elements. We prove its completeness by a PER model and its soundness by a Kripke logical relation.
We show that a version of Martin-Löf type theory with an extensional identity type former I, a unit type N1 , Sigma-types, Pi-types, and a base type is a free …
We show that a version of Martin-Löf type theory with an extensional identity type former I, a unit type N1 , Sigma-types, Pi-types, and a base type is a free category with families (supporting these type formers) both in a 1- and a 2-categorical sense. It follows that the underlying category of contexts is a free locally cartesian closed category in a 2-categorical sense because of a previously proved biequivalence. We show that equality in this category is undecidable by reducing it to the undecidability of convertibility in combinatory logic. Essentially the same construction also shows a slightly strengthened form of the result that equality in extensional Martin-Löf type theory with one universe is undecidable.
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.
We show that a version of Martin-L\of type theory with extensional identity, a unit type N_1, {\Sigma}, {\Pi},and a base type is a free category with families (supporting these type …
We show that a version of Martin-L\of type theory with extensional identity, a unit type N_1, {\Sigma}, {\Pi},and a base type is a free category with families (supporting these type formers) both in a 1- and a 2-categorical sense. It follows that the underlying category of contexts is a free locally cartesian closed category in a 2-categorical sense because of a previously proved biequivalence. We then show that equality in this category is undecidable by reducing it to the undecidability of convertibility in combinatory logic.
We give a new syntax independent definition of the notion of a generalized algebraic theory as an initial object in a category of categories with families (cwfs) with extra structure. …
We give a new syntax independent definition of the notion of a generalized algebraic theory as an initial object in a category of categories with families (cwfs) with extra structure. To this end we define inductively how to build a valid signature $Σ$ for a generalized algebraic theory and the associated category of cwfs with a $Σ$-structure and cwf-morphisms that preserve this structure on the nose. Our definition refers to uniform families of contexts, types, and terms, a purely semantic notion. Furthermore, we show how to syntactically construct initial cwfs with $Σ$-structures. This result can be viewed as a generalization of Birkhoff's completeness theorem for equational logic. It is obtained by extending Castellan, Clairambault, and Dybjer's construction of an initial cwf. We provide examples of generalized algebraic theories for monoids, categories, categories with families, and categories with families with extra structure for some type formers of dependent type theory. The models of these are internal monoids, internal categories, and internal categories with families (with extra structure) in a category with families.
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.
The aim of this paper is to refine and extend proposals by Sozeau and Tabareau and by Voevodsky for universe polymorphism in type theory. In those systems judgments can depend …
The aim of this paper is to refine and extend proposals by Sozeau and Tabareau and by Voevodsky for universe polymorphism in type theory. In those systems judgments can depend on explicit constraints between universe levels. We here present a system where we also have products indexed by universe levels and by constraints. Our theory has judgments for internal universe levels, built up from level variables by a successor operation and a binary supremum operation, and also judgments for equality of universe levels.
The aim of this paper is to refine and extend proposals by Sozeau and Tabareau and by Voevodsky for universe polymorphism in type theory. In those systems judgments can depend …
The aim of this paper is to refine and extend proposals by Sozeau and Tabareau and by Voevodsky for universe polymorphism in type theory. In those systems judgments can depend on explicit constraints between universe levels. We here present a system where we also have products indexed by universe levels and by constraints. Our theory has judgments for internal universe levels, built up from level variables by a successor operation and a binary supremum operation, and also judgments for equality of universe levels.
We give a new syntax independent definition of the notion of a generalized algebraic theory as an initial object in a category of categories with families (cwfs) with extra structure. …
We give a new syntax independent definition of the notion of a generalized algebraic theory as an initial object in a category of categories with families (cwfs) with extra structure. To this end we define inductively how to build a valid signature $Σ$ for a generalized algebraic theory and the associated category of cwfs with a $Σ$-structure and cwf-morphisms that preserve this structure on the nose. Our definition refers to uniform families of contexts, types, and terms, a purely semantic notion. Furthermore, we show how to syntactically construct initial cwfs with $Σ$-structures. This result can be viewed as a generalization of Birkhoff's completeness theorem for equational logic. It is obtained by extending Castellan, Clairambault, and Dybjer's construction of an initial cwf. We provide examples of generalized algebraic theories for monoids, categories, categories with families, and categories with families with extra structure for some type formers of dependent type theory. The models of these are internal monoids, internal categories, and internal categories with families (with extra structure) in a category with families.
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.
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.
A higher inductive type of level 1 (a 1-hit) has constructors for points and paths only, whereas a higher inductive type of level 2 (a 2-hit) has constructors for surfaces …
A higher inductive type of level 1 (a 1-hit) has constructors for points and paths only, whereas a higher inductive type of level 2 (a 2-hit) has constructors for surfaces too. We restrict attention to finitary higher inductive types and present general schemata for the types of their point, path, and surface constructors. We also derive the elimination and equality rules from the types of constructors for 1-hits and 2-hits. Moreover, we construct a groupoid model for dependent type theory with 2-hits and point out that we obtain a setoid model for dependent type theory with 1-hits by truncating the groupoid model.
We show that a version of Martin-L\of type theory with extensional identity, a unit type N_1, {\Sigma}, {\Pi},and a base type is a free category with families (supporting these type …
We show that a version of Martin-L\of type theory with extensional identity, a unit type N_1, {\Sigma}, {\Pi},and a base type is a free category with families (supporting these type formers) both in a 1- and a 2-categorical sense. It follows that the underlying category of contexts is a free locally cartesian closed category in a 2-categorical sense because of a previously proved biequivalence. We then show that equality in this category is undecidable by reducing it to the undecidability of convertibility in combinatory logic.
We show that a version of Martin-Löf type theory with an extensional identity type former I, a unit type N1 , Sigma-types, Pi-types, and a base type is a free …
We show that a version of Martin-Löf type theory with an extensional identity type former I, a unit type N1 , Sigma-types, Pi-types, and a base type is a free category with families (supporting these type formers) both in a 1- and a 2-categorical sense. It follows that the underlying category of contexts is a free locally cartesian closed category in a 2-categorical sense because of a previously proved biequivalence. We show that equality in this category is undecidable by reducing it to the undecidability of convertibility in combinatory logic. Essentially the same construction also shows a slightly strengthened form of the result that equality in extensional Martin-Löf type theory with one universe is undecidable.
Seely's paper "Locally cartesian closed categories and type theory" contains a well-known result in categorical type theory: that the category of locally cartesian closed categories is equivalent to the category …
Seely's paper "Locally cartesian closed categories and type theory" contains a well-known result in categorical type theory: that the category of locally cartesian closed categories is equivalent to the category of Martin-L\"of type theories with Pi-types, Sigma-types and extensional identity types. However, Seely's proof relies on the problematic assumption that substitution in types can be interpreted by pullbacks. Here we prove a corrected version of Seely's theorem: that the B\'enabou-Hofmann interpretation of Martin-L\"of type theory in locally cartesian closed categories yields a biequivalence of 2-categories. To facilitate the technical development we employ categories with families as a substitute for syntactic Martin-L\"of type theories. As a second result we prove that if we remove Pi-types the resulting categories with families are biequivalent to left exact categories.
Homotopy type theory is a new branch of mathematics, based on a recently discovered connection between homotopy theory and type theory, which brings new ideas into the very foundation of …
Homotopy type theory is a new branch of mathematics, based on a recently discovered connection between homotopy theory and type theory, which brings new ideas into the very foundation of mathematics. On the one hand, Voevodsky's subtle and beautiful "univalence axiom" implies that isomorphic structures can be identified. On the other hand, "higher inductive types" provide direct, logical descriptions of some of the basic spaces and constructions of homotopy theory. Both are impossible to capture directly in classical set-theoretic foundations, but when combined in homotopy type theory, they permit an entirely new kind of "logic of homotopy types". This suggests a new conception of foundations of mathematics, with intrinsic homotopical content, an "invariant" conception of the objects of mathematics -- and convenient machine implementations, which can serve as a practical aid to the working mathematician. This book is intended as a first systematic exposition of the basics of the resulting "Univalent Foundations" program, and a collection of examples of this new style of reasoning -- but without requiring the reader to know or learn any formal logic, or to use any computer proof assistant.
We present an algorithm for computing normal terms and types in Martin-Löf type theory with one universe and eta-conversion. We prove that two terms or types are equal in the …
We present an algorithm for computing normal terms and types in Martin-Löf type theory with one universe and eta-conversion. We prove that two terms or types are equal in the theory iff the normal forms are identical (as de Bruijn terms). It thus follows that our algorithm can be used for deciding equality in Martin-Löf type theory. The algorithm uses the technique of normalization by evaluation; normal forms are computed by first evaluating terms and types in a suitable model. The normal forms are then extracted from the semantic elements. We prove its completeness by a PER model and its soundness by a Kripke logical relation.
We show how to solve the word problem for simply typed λβη-calculus by using a few well-known facts about categories of presheaves and the Yoneda embedding. The formal setting for …
We show how to solve the word problem for simply typed λβη-calculus by using a few well-known facts about categories of presheaves and the Yoneda embedding. The formal setting for these results is [Pscr ]-category theory, a version of ordinary category theory where each hom-set is equipped with a partial equivalence relation. The part of [Pscr ]-category theory we develop here is constructive and thus permits extraction of programs from proofs. It is important to stress that in our method we make no use of traditional proof-theoretic or rewriting techniques. To show the robustness of our method, we give an extended treatment for more general λ-theories in the Appendix.
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 .
Any attempt to give “foundations”, for category theory or any domain in mathematics, could have two objectives, of course related. (0.1) Noncontradiction : Namely, to provide a formal frame rich …
Any attempt to give “foundations”, for category theory or any domain in mathematics, could have two objectives, of course related. (0.1) Noncontradiction : Namely, to provide a formal frame rich enough so that all the actual activity in the domain can be carried out within this frame, and consistent, or at least relatively consistent with a well-established and “safe” theory, e.g. Zermelo-Frankel (ZF). (0.2) Adequacy , in the following, nontechnical sense: (i) The basic notions must be simple enough to make transparent the syntactic structures involved. (ii) The translation between the formal language and the usual language must be, or very quickly become, obvious. This implies in particular that the terminology and notations in the formal system should be identical, or very similar, to the current ones. Although this may seem minor, it is in fact very important. (iii) “Foundations” can only be “foundations of a given domain at a given moment”, therefore the frame should be easily adaptable to extensions or generalizations of the domain, and, even better, in view of (i), it should suggest how to find meaningful generalizations. (iv) Sometimes (ii) and (iii) can be incompatible because the current notations are not adapted to a more general situation. A compromise is then necessary. Usually when the tradition is very strong (ii) is predominant, but this causes some incoherence for the notations in the more general case (e.g. the notation f ( x ) for the value of a function f at x obliges one, in category theory, to denote the composition of arrows ( f, g ) → g∘f , and all attempts to change this notation have, so far, failed).
A concise guide to very basic bicategory theory, from the definition of a bicategory to the coherence theorem.
A concise guide to very basic bicategory theory, from the definition of a bicategory to the coherence theorem.
We show that a version of Martin-Löf type theory with an extensional identity type former I, a unit type N1 , Sigma-types, Pi-types, and a base type is a free …
We show that a version of Martin-Löf type theory with an extensional identity type former I, a unit type N1 , Sigma-types, Pi-types, and a base type is a free category with families (supporting these type formers) both in a 1- and a 2-categorical sense. It follows that the underlying category of contexts is a free locally cartesian closed category in a 2-categorical sense because of a previously proved biequivalence. We show that equality in this category is undecidable by reducing it to the undecidability of convertibility in combinatory logic. Essentially the same construction also shows a slightly strengthened form of the result that equality in extensional Martin-Löf type theory with one universe is undecidable.
Seely's paper "Locally cartesian closed categories and type theory" contains a well-known result in categorical type theory: that the category of locally cartesian closed categories is equivalent to the category …
Seely's paper "Locally cartesian closed categories and type theory" contains a well-known result in categorical type theory: that the category of locally cartesian closed categories is equivalent to the category of Martin-L\"of type theories with Pi-types, Sigma-types and extensional identity types. However, Seely's proof relies on the problematic assumption that substitution in types can be interpreted by pullbacks. Here we prove a corrected version of Seely's theorem: that the B\'enabou-Hofmann interpretation of Martin-L\"of type theory in locally cartesian closed categories yields a biequivalence of 2-categories. To facilitate the technical development we employ categories with families as a substitute for syntactic Martin-L\"of type theories. As a second result we prove that if we remove Pi-types the resulting categories with families are biequivalent to left exact categories.
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.
Homotopy type theory is an interpretation of Martin-Lof's constructive type theory into abstract homotopy theory. There results a link between constructive mathematics and algebraic topology, providing topological semantics for intensional …
Homotopy type theory is an interpretation of Martin-Lof's constructive type theory into abstract homotopy theory. There results a link between constructive mathematics and algebraic topology, providing topological semantics for intensional systems of type theory as well as a computational approach to algebraic topology via type theory-based proof assistants such as Coq. The present work investigates inductive types in this setting. Modified rules for inductive types, including types of well-founded trees, or W-types, are presented, and the basic homotopical semantics of such types are determined. Proofs of all results have been formally verified by the Coq proof assistant, and the proof scripts for this verification form an essential component of this research.
It is shown that an intuitionistic model of set theory with the axiom of choice has to be a classical one.
It is shown that an intuitionistic model of set theory with the axiom of choice has to be a classical one.
The following paper is a study of abstract algebras qua abstract algebras. As no vocabulary suitable for this purpose is current, I have been forced to use a number of …
The following paper is a study of abstract algebras qua abstract algebras. As no vocabulary suitable for this purpose is current, I have been forced to use a number of new terms, and extend the meaning of some accepted ones.
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.
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.
Is it reasonable to do constructive mathematics without the axiom of countable choice?Serious schools of constructive mathematics all assume it one way or another, but the arguments for it are …
Is it reasonable to do constructive mathematics without the axiom of countable choice?Serious schools of constructive mathematics all assume it one way or another, but the arguments for it are not compelling.The fundamental theorem of algebra will serve as an example of where countable choice comes into play and how to proceed in its absence.Along the way, a notion of a complete metric space, suitable for a choiceless environment, is developed.
We present a new approach to introducing an extensional propositional equality in Intensional Type Theory. Our construction is based on the observation that there is a sound, intensional setoid model …
We present a new approach to introducing an extensional propositional equality in Intensional Type Theory. Our construction is based on the observation that there is a sound, intensional setoid model in Intensional Type theory with a proof-irrelevant universe of propositions and /spl eta/-rules for /spl Pi/and /spl Sigma/-types. The Type Theory corresponding to this model is decidable, has no irreducible constants and permits large eliminations, which are essential for universes.
We show that Hofmann's and Curien's interpretations of Martin-Löf's type theory, which were both designed to cure a mismatch between syntax and semantics in Seely's original interpretation in locally cartesian …
We show that Hofmann's and Curien's interpretations of Martin-Löf's type theory, which were both designed to cure a mismatch between syntax and semantics in Seely's original interpretation in locally cartesian closed categories, are related via a natural isomorphism. As an outcome, we obtain a new proof of the coherence theorem needed to show the soundness after all of Seely's interpretation.
Setoids commonly take the place of sets when formalising mathematics inside type theory. In this note, the category of setoids is studied in type theory with universes that are as …
Setoids commonly take the place of sets when formalising mathematics inside type theory. In this note, the category of setoids is studied in type theory with universes that are as small as possible (and thus, the type theory is as weak as possible). In particular, we will consider epimorphisms and disjoint sums. We show that, given the minimal type universe, all epimorphisms are surjections, and disjoint sums exist. Further, without universes, there are countermodels for these statements, and if we use the Logical Framework formulation of type theory, these statements are provably non-derivable.
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.
Quotient inductive-inductive types (QIITs) generalise inductive types in two ways: a QIIT can have more than one sort and the later sorts can be indexed over the previous ones. In …
Quotient inductive-inductive types (QIITs) generalise inductive types in two ways: a QIIT can have more than one sort and the later sorts can be indexed over the previous ones. In addition, equality constructors are also allowed. We work in a setting with uniqueness of identity proofs, hence we use the term QIIT instead of higher inductive-inductive type. An example of a QIIT is the well-typed (intrinsic) syntax of type theory quotiented by conversion. In this paper first we specify finitary QIITs using a domain-specific type theory which we call the theory of signatures. The syntax of the theory of signatures is given by a QIIT as well. Then, using this syntax we show that all specified QIITs exist and they have a dependent elimination principle. We also show that algebras of a signature form a category with families (CwF) and use the internal language of this CwF to show that dependent elimination is equivalent to initiality.
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.
In this paper, we analyze and compare three of the many algebraic structures that have been used for modeling dependent type theories: categories with families, split type-categories, and representable maps …
In this paper, we analyze and compare three of the many algebraic structures that have been used for modeling dependent type theories: categories with families, split type-categories, and representable maps of presheaves. We study these in univalent type theory, where the comparisons between them can be given more elementarily than in set-theoretic foundations. Specifically, we construct maps between the various types of structures, and show that assuming the Univalence axiom, some of the comparisons are equivalences. We then analyze how these structures transfer along (weak and strong) equivalences of categories, and, in particular, show how they descend from a category (not assumed univalent/saturated) to its Rezk completion. To this end, we introduce relative universes, generalizing the preceding notions, and study the transfer of such relative universes along suitable structure. We work throughout in (intensional) dependent type theory; some results, but not all, assume the univalence axiom. All the material of this paper has been formalized in Coq, over the UniMath library.
Bishop's informal set theory is briefly discussed and compared to Lawvere's Elementary Theory of the Category of Sets (ETCS). We then present a constructive and predicative version of ETCS, whose …
Bishop's informal set theory is briefly discussed and compared to Lawvere's Elementary Theory of the Category of Sets (ETCS). We then present a constructive and predicative version of ETCS, whose standard model is based on the constructive type theory of Martin-Lof. The theory, CETCS, provides a structuralist foundation for constructive mathematics in the style of Bishop.
The notion of a natural model of type theory is defined in terms of that of a representable natural transfomation of presheaves. It is shown that such models agree exactly …
The notion of a natural model of type theory is defined in terms of that of a representable natural transfomation of presheaves. It is shown that such models agree exactly with the concept of a category with families in the sense of Dybjer, which can be regarded as an algebraic formulation of type theory. We determine conditions for such models to satisfy the inference rules for dependent sums Σ, dependent products Π and intensional identity types Id , as used in homotopy type theory. It is then shown that a category admits such a model if it has a class of maps that behave like the abstract fibrations in axiomatic homotopy theory: They should be stable under pullback, closed under composition and relative products, and there should be weakly orthogonal factorizations into the class. It follows that many familiar settings for homotopy theory also admit natural models of the basic system of homotopy type theory.
Postulating an impredicative universe in dependent type theory allows System F style encodings of finitary inductive types, but these fail to satisfy the relevant η-equalities and consequently do not admit …
Postulating an impredicative universe in dependent type theory allows System F style encodings of finitary inductive types, but these fail to satisfy the relevant η-equalities and consequently do not admit dependent eliminators. To recover η and dependent elimination, we present a method to construct refinements of these impredicative encodings, using ideas from homotopy type theory. We then extend our method to construct impredicative encodings of some higher inductive types, such as 1-truncation and the unit circle S1.
The theory developed by Gambino and Kock, of polynomials over a locally cartesian closed categoryE, is generalised forE just having pullbacks. The 2-categorical analogue of the theory of polynomials and …
The theory developed by Gambino and Kock, of polynomials over a locally cartesian closed categoryE, is generalised forE just having pullbacks. The 2-categorical analogue of the theory of polynomials and polynomial functors is given, and its rela- tionship with Street's theory of brations within 2-categories is explored. Johnstone's notion of \bagdomain data is adapted to the present framework to make it easier to completely exhibit examples of polynomial monads.
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.
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.
The theory of types with which we shall be concerned is intended to be a full scale system for formalizing intuitionistic mathematics as developed, for example, in the book by …
The theory of types with which we shall be concerned is intended to be a full scale system for formalizing intuitionistic mathematics as developed, for example, in the book by Bishop 1967. The language of the theory is richer than the language of first order predicate logic. This makes it possible to strengthen the axioms for existence and disjunction. In the case of existence, the possibility of strengthening the usual elimination rule seems first to have been indicated by Howard 1969, whose proposed axioms are special cases of the existential elimination rule of the present theory. Furthermore, there is a reflection principle which links the generation of objects and types and plays somewhat the same role for the present theory as does the replacement axiom for Zermelo-Fraenkel set theory. An earlier, not yet conclusive, attempt at formulating a theory of this kind was made by Scott 1970. Also related, although less closely, are the type and logic free theories of constructions of Kreisel 1962 and 1965 and Goodman 1970. In its first version, the present theory was based on the strongly impredicative axiom that there is a type of all types whatsoever, which is at the same time a type and an object of that type. This axiom had to be abandoned, however, after it was shown to lead to a contradiction by Jean Yves Girard. I am very grateful to him for showing me his paradox. The change that it necessitated is so drastic that my theory no longer contains intuitionistic simple type theory as it originally did. Instead, its proof theoretic strength should be close to that of predicative analysis. Mathematical objects and their types. We shall think of mathematical objects or constructions. Every mathematical object is of a certain kind or type. Better, a mathematical object is always given together with its type, that is, it is not just an object, it is an object of a certain type.
We implement in the formal language of homotopy type theory a new set of axioms called cohesion. Then we indicate how the resulting cohesive homotopy type theory naturally serves as …
We implement in the formal language of homotopy type theory a new set of axioms called cohesion. Then we indicate how the resulting cohesive homotopy type theory naturally serves as a formal foundation for central concepts in quantum gauge field theory. This is a brief survey of work by the authors developed in detail elsewhere.
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.