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 study polynomial functors over locally cartesian closed categories. After setting up the basic theory, we show how polynomial functors assemble into a double category, in fact a framed bicategory. …
We study polynomial functors over locally cartesian closed categories. After setting up the basic theory, we show how polynomial functors assemble into a double category, in fact a framed bicategory. We show that the free monad on a polynomial endofunctor is polynomial. The relationship with operads and other related notions is explored.
The concept of generalised species of structures between small categories and, correspondingly, that of generalised analytic functor between presheaf categories are introduced. An operation of substitution for generalised species, which …
The concept of generalised species of structures between small categories and, correspondingly, that of generalised analytic functor between presheaf categories are introduced. An operation of substitution for generalised species, which is the counterpart to the composition of generalised analytic functors, is also put forward. These definitions encompass most notions of combinatorial species considered in the literature — including of course Joyal's original notion — together with their associated substitution operation. Our first main result exhibits the substitution calculus of generalised species as arising from a Kleisli bicategory for a pseudo-comonad on profunctors. Our second main result establishes that the bicategory of generalised species of structures is cartesian closed.
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.
We develop further the theory of weak factorization systems and algebraic weak factorization systems. In particular, we give a method for constructing (algebraic) weak factorization systems whose right maps can …
We develop further the theory of weak factorization systems and algebraic weak factorization systems. In particular, we give a method for constructing (algebraic) weak factorization systems whose right maps can be thought of as (uniform) fibrations and that satisfy the (functorial) Frobenius condition. As applications, we obtain a new proof that the Quillen model structure for Kan complexes is right proper, avoiding entirely the use of topological realization and minimal fibrations, and we solve an open problem in the study of Voevodsky's simplicial model of type theory, proving a constructive version of the preservation of Kan fibrations by pushforward along Kan fibrations. Our results also subsume and extend work by Coquand and others on cubical sets.
We develop further the theory of operads and analytic functors.In particular, we introduce the bicategory OpdBim V of operad bimodules, that has operads as 0-cells, operad bimodules as 1-cells and …
We develop further the theory of operads and analytic functors.In particular, we introduce the bicategory OpdBim V of operad bimodules, that has operads as 0-cells, operad bimodules as 1-cells and operad bimodule maps as 2-cells, and prove that it is cartesian closed.In order to obtain this result, we extend the theory of distributors and the formal theory of monads.
We define what it means for a formal topology to be spatial, and investigate properties related to spatiality both in general and in examples.
We define what it means for a formal topology to be spatial, and investigate properties related to spatiality both in general and in examples.
We introduce the notion of a relative pseudomonad, which generalizes the notion of a pseudomonad, and define the Kleisli bicategory associated to a relative pseudomonad. We then present an efficient …
We introduce the notion of a relative pseudomonad, which generalizes the notion of a pseudomonad, and define the Kleisli bicategory associated to a relative pseudomonad. We then present an efficient method to define pseudomonads on the Kleisli bicategory of a relative pseudomonad. The results are applied to define several pseudomonads on the bicategory of profunctors in an homogeneous way and provide a uniform approach to the definition of bicategories that are of interest in operad theory, mathematical logic, and theoretical computer science.
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.
We investigate inductive types in type theory, using the insights provided by homotopy type theory and univalent foundations of mathematics. We do so by introducing the new notion of a …
We investigate inductive types in type theory, using the insights provided by homotopy type theory and univalent foundations of mathematics. We do so by introducing the new notion of a homotopy-initial algebra. This notion is defined by a purely type-theoretic contractibility condition that replaces the standard, category-theoretic universal property involving the existence and uniqueness of appropriate morphisms. Our main result characterizes the types that are equivalent to W-types as homotopy-initial algebras.
Abstract This chapter introduces new kinds of models for constructive set theories based on categories of presheaves. It concentrates on categories of classes rather than sets, following the lines of …
Abstract This chapter introduces new kinds of models for constructive set theories based on categories of presheaves. It concentrates on categories of classes rather than sets, following the lines of algebraic set theory. It defines a general notion of what is a categorical model for CST, and shows that categories of presheaves provide examples of such models. To do so, it considers presheaves as functors with values in a category of classes. The models introduced are a counterpart of the presheaf models for intuitionistic set theories defined by Dana Scott in the 1980s. In this work, the author has to overcome the challenges intrinsic to dealing with generalized predicative formal systems rather than impredicative ones. An application to an independence result is discussed.
We provide a partial solution to the problem of defining a constructive version of Voevodsky's simplicial model of Univalent Foundations. For this, we prove constructive counterparts of the necessary results …
We provide a partial solution to the problem of defining a constructive version of Voevodsky's simplicial model of Univalent Foundations. For this, we prove constructive counterparts of the necessary results of simplicial homotopy theory, building on the constructive version of the Kan-Quillen model structure established by the second-named author. In particular, we show that dependent products along fibrations with cofibrant domains preserve fibrations, establish the weak equivalence extension property for weak equivalences between fibrations with cofibrant domain and define a univalent fibration that classifies small fibrations between bifibrant objects. These results allow us to define a comprehension category supporting identity types, Σ $\Sigma$ -types, Π $\Pi$ -types and a univalent universe, leaving only a coherence question to be addressed.
We present a solution to the problem of defining a counterpart in Algebraic Set Theory of the construction of internal sheaves in Topos Theory. Our approach is general in that …
We present a solution to the problem of defining a counterpart in Algebraic Set Theory of the construction of internal sheaves in Topos Theory. Our approach is general in that we consider sheaves as determined by Lawvere-Tierney coverages, rather than by Grothendieck coverages, and assume only a weakening of the axioms for small maps originally introduced by Joyal and Moerdijk, thus subsuming the existing topos-theoretic results.
We characterize double adjunctions in terms of presheaves and universal squares, and then apply these characterizations to free monads and Eilenberg--Moore objects in double categories. We improve upon our earlier …
We characterize double adjunctions in terms of presheaves and universal squares, and then apply these characterizations to free monads and Eilenberg--Moore objects in double categories. We improve upon our earlier result in Monads in Double Categories, JPAA 215:6, pages 1174-1197, 2011, to conclude: if a double category with cofolding admits the construction of free monads in its horizontal 2-category, then it also admits the construction of free monads as a double category. We also prove that a double category admits Eilenberg--Moore objects if and only if a certain parameterized presheaf is representable. Along the way, we develop parameterized presheaves on double categories and prove a double-categorical Yoneda Lemma.
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.
We introduce and study the notion of a uniform fibration in categories with a functorial cylinder. In particular, we show that in a wide class of presheaf categories, including simplicial …
We introduce and study the notion of a uniform fibration in categories with a functorial cylinder. In particular, we show that in a wide class of presheaf categories, including simplicial sets and cubical sets with connections, uniform fibrations are the right class of a natural weak factorization system and satisfy the Frobenius condition. This implies that pushforward along a uniform fibration preserves uniform fibrations. When instantiated in simplicial sets, this result gives a constructive counterpart of one of the key facts underpinning Voevodsky's simplicial model of univalent foundations, while in cubical sets it extends some of the existing work on cubical models of type theory by Coquand and others.
We present two new proofs of Simon Henry's result that the category of simplicial sets admits a constructive counterpart of the classical Kan-Quillen model structure. Our proofs are entirely self-contained …
We present two new proofs of Simon Henry's result that the category of simplicial sets admits a constructive counterpart of the classical Kan-Quillen model structure. Our proofs are entirely self-contained and avoid complex combinatorial arguments on anodyne extensions. We also give new constructive proofs of the left and right properness of the model structure.
Abstract We present two new proofs of Simon Henry’s result that the category of simplicial sets admits a constructive counterpart of the classical Kan–Quillen model structure. Our proofs are entirely …
Abstract We present two new proofs of Simon Henry’s result that the category of simplicial sets admits a constructive counterpart of the classical Kan–Quillen model structure. Our proofs are entirely self-contained and avoid complex combinatorial arguments on anodyne extensions. We also give new constructive proofs of the left and right properness of the model structure.
We introduce type-theoretic algebraic weak factorisation systems and show how they give rise to homotopy-theoretic models of Martin-Lof type theory. This is done by showing that the comprehension category associated …
We introduce type-theoretic algebraic weak factorisation systems and show how they give rise to homotopy-theoretic models of Martin-Lof type theory. This is done by showing that the comprehension category associated to a type-theoretic algebraic weak factorisation system satisfies the assumptions necessary to apply a right adjoint method for splitting comprehension categories. We then provide methods for constructing several examples of type-theoretic algebraic weak factorisation systems, encompassing the existing groupoid model and cubical sets models, as well as some models based on normal fibrations
We introduce type-theoretic algebraic weak factorisation systems and show how they give rise to homotopy-theoretic models of Martin-L\"of type theory. This is done by showing that the comprehension category associated …
We introduce type-theoretic algebraic weak factorisation systems and show how they give rise to homotopy-theoretic models of Martin-L\"of type theory. This is done by showing that the comprehension category associated to a type-theoretic algebraic weak factorisation system satisfies the assumptions necessary to apply a right adjoint method for splitting comprehension categories. We then provide methods for constructing several examples of type-theoretic algebraic weak factorisation systems, encompassing the existing groupoid model and cubical sets models, as well as some models based on normal fibrations
We introduce a new method for precisely relating certain kinds of algebraic structures in a presheaf category and judgements of its internal type theory. The method provides a systematic way …
We introduce a new method for precisely relating certain kinds of algebraic structures in a presheaf category and judgements of its internal type theory. The method provides a systematic way to organise complex diagrammatic reasoning and generalises the well-known Kripke-Joyal forcing for logic. As an application, we prove several properties of algebraic weak factorisation systems considered in Homotopy Type Theory.
We characterize double adjunctions in terms of presheaves and universal squares, and then apply these characterizations to free monads and Eilenberg--Moore objects in double categories. We improve upon our earlier …
We characterize double adjunctions in terms of presheaves and universal squares, and then apply these characterizations to free monads and Eilenberg--Moore objects in double categories. We improve upon our earlier result in "Monads in Double Categories", JPAA 215:6, pages 1174-1197, 2011, to conclude: if a double category with cofolding admits the construction of free monads in its horizontal 2-category, then it also admits the construction of free monads as a double category. We also prove that a double category admits Eilenberg--Moore objects if and only if a certain parameterized presheaf is representable. Along the way, we develop parameterized presheaves on double categories and prove a double-categorical Yoneda Lemma.
For a category $\mathcal E$ with finite limits and well-behaved countable coproducts, we construct a model structure, called the effective model structure, on the category of simplicial objects in $\mathcal …
For a category $\mathcal E$ with finite limits and well-behaved countable coproducts, we construct a model structure, called the effective model structure, on the category of simplicial objects in $\mathcal E$, generalising the Kan--Quillen model structure on simplicial sets. We then prove that the effective model structure is left and right proper and satisfies descent in the sense of Rezk. As a consequence, we obtain that the associated $\infty$-category has finite limits, colimits satisfying descent, and is locally Cartesian closed when $\mathcal E$ is, but is not a higher topos in general. We also characterise the $\infty$-category presented by the effective model structure, showing that it is the full sub-category of presheaves on $\mathcal E$ spanned by Kan complexes in $\mathcal E$, a result that suggests a close analogy with the theory of exact completions.
We extend the arithmetic product of species of structures and symmetric sequences studied by Maia and Mendez and by Dwyer and Hess to coloured symmetric sequences and show that it …
We extend the arithmetic product of species of structures and symmetric sequences studied by Maia and Mendez and by Dwyer and Hess to coloured symmetric sequences and show that it determines a normal oplax monoidal structure on the bicategory of coloured symmetric sequences. In order to do this, we establish general results on extending monoidal structures to Kleisli bicategories. Our approach uses monoidal double categories, which help us to attack the difficult problem of verifying the coherence conditions for a monoidal bicategory in an efficient way.
Abstract For a category $\mathcal {E}$ with finite limits and well-behaved countable coproducts, we construct a model structure, called the effective model structure, on the category of simplicial objects in …
Abstract For a category $\mathcal {E}$ with finite limits and well-behaved countable coproducts, we construct a model structure, called the effective model structure, on the category of simplicial objects in $\mathcal {E}$ , generalising the Kan–Quillen model structure on simplicial sets. We then prove that the effective model structure is left and right proper and satisfies descent in the sense of Rezk. As a consequence, we obtain that the associated $\infty $ -category has finite limits, colimits satisfying descent, and is locally Cartesian closed when $\mathcal {E}$ is but is not a higher topos in general. We also characterise the $\infty $ -category presented by the effective model structure, showing that it is the full sub-category of presheaves on $\mathcal {E}$ spanned by Kan complexes in $\mathcal {E}$ , a result that suggests a close analogy with the theory of exact completions.
We extend the arithmetic product of species of structures and symmetric sequences studied by Maia and Méndez and by Dwyer and Hess to coloured symmetric sequences and show that it …
We extend the arithmetic product of species of structures and symmetric sequences studied by Maia and Méndez and by Dwyer and Hess to coloured symmetric sequences and show that it determines a normal oplax monoidal structure on the bicategory of coloured symmetric sequences. In order to do this, we establish general results on extending monoidal structures to Kleisli bicategories. Our approach uses monoidal double categories, which help us to attack the difficult problem of verifying the coherence conditions for a monoidal bicategory in an efficient way.
We investigate inductive types in type theory, using the insights provided by homotopy type theory and univalent foundations of mathematics. We do so by introducing the new notion of a …
We investigate inductive types in type theory, using the insights provided by homotopy type theory and univalent foundations of mathematics. We do so by introducing the new notion of a homotopy-initial algebra. This notion is defined by a purely type-theoretic contractibility condition which replaces the standard, category-theoretic universal property involving the existence and uniqueness of appropriate morphisms. Our main result characterises the types that are equivalent to W-types as homotopy-initial algebras.
We give an overview of the main ideas involved in the development of homotopy type theory and the univalent foundations of Mathematics programme. This serves as a background for the …
We give an overview of the main ideas involved in the development of homotopy type theory and the univalent foundations of Mathematics programme. This serves as a background for the research papers published in the special issue.
We extend the basic concepts of Street's formal theory of monads from the setting of 2-categories to that of double categories. In particular, we introduce the double category Mnd(C) of …
We extend the basic concepts of Street's formal theory of monads from the setting of 2-categories to that of double categories. In particular, we introduce the double category Mnd(C) of monads in a double category C and define what it means for a double category to admit the construction of free monads. Our main theorem shows that, under some mild conditions, a double category that is a framed bicategory admits the construction of free monads if its horizontal 2-category does. We apply this result to obtain double adjunctions which extend the adjunction between graphs and categories and the adjunction between polynomial endofunctors and polynomial monads.
We contribute to the formal theory of pseudomonads, i.e. the analogue for pseudomonads of the formal theory of monads. In particular, we solve a problem posed by Steve Lack by …
We contribute to the formal theory of pseudomonads, i.e. the analogue for pseudomonads of the formal theory of monads. In particular, we solve a problem posed by Steve Lack by proving that, for every Gray-category K, there is a Gray-category Psm(K) of pseudomonads, pseudomonad morphisms, pseudomonad transformations and pseudomonad modifications in K. We then establish a triequivalence between Psm(K) and the Gray-category of pseudomonads introduced by Marmolejo. Finally, these results are applied to give a clear account of the coherence conditions for pseudodistributive laws. 41 pages. Comments welcome.
Homotopy type theory is an interpretation of Martin-Löf'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-Löf'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.
We extend the basic concepts of Street's formal theory of monads from the setting of 2-categories to that of double categories. In particular, we introduce the double category Mnd(C) of …
We extend the basic concepts of Street's formal theory of monads from the setting of 2-categories to that of double categories. In particular, we introduce the double category Mnd(C) of monads in a double category C and define what it means for a double category to admit the construction of free monads. Our main theorem shows that, under some mild conditions, a double category that is a framed bicategory admits the construction of free monads if its horizontal 2-category does. We apply this result to obtain double adjunctions which extend the adjunction between graphs and categories and the adjunction between polynomial endofunctors and polynomial monads.
We investigate inductive types in type theory, using the insights provided by homotopy type theory and univalent foundations of mathematics. We do so by introducing the new notion of a …
We investigate inductive types in type theory, using the insights provided by homotopy type theory and univalent foundations of mathematics. We do so by introducing the new notion of a homotopy-initial algebra. This notion is defined by a purely type-theoretic contractibility condition which replaces the standard, category-theoretic universal property involving the existence and uniqueness of appropriate morphisms. Our main result characterises the types that are equivalent to W-types as homotopy-initial algebras.
We show that the classifying category C(T) of a dependent type theory T with axioms for identity types admits a non-trivial weak factorisation system. We provide an explicit characterisation of …
We show that the classifying category C(T) of a dependent type theory T with axioms for identity types admits a non-trivial weak factorisation system. We provide an explicit characterisation of the elements of both the left class and the right class of the weak factorisation system. This characterisation is applied to relate identity types and the homotopy theory of groupoids.
We develop further the theory of monoidal bicategories by introducing and studying bicate- gorical counterparts of the notions of a linear explonential comonad, as considered in the study of linear …
We develop further the theory of monoidal bicategories by introducing and studying bicate- gorical counterparts of the notions of a linear explonential comonad, as considered in the study of linear logic, and of a codereliction transformation, introduced to study differential linear logic via differential categories. As an application, we extend the differential calculus of Joyal's analytic functors to analytic functors between presheaf categories, just as ordinary calculus extends from a single variable to many variables.
Abstract We introduce a new method for precisely relating algebraic structures in a presheaf category and judgements of its internal type theory. The method provides a systematic way to organise …
Abstract We introduce a new method for precisely relating algebraic structures in a presheaf category and judgements of its internal type theory. The method provides a systematic way to organise complex diagrammatic reasoning and generalises the well-known Kripke-Joyal forcing for logic. As an application, we prove several properties of algebraic weak factorisation systems considered in Homotopy Type Theory.
Abstract We give a brief overview of the special issue of MSCS “Advances in Homotopy Type Theory.”
Abstract We give a brief overview of the special issue of MSCS “Advances in Homotopy Type Theory.”
Abstract We give a brief overview of the special issue of MSCS “Advances in Homotopy Type Theory.”
Abstract We give a brief overview of the special issue of MSCS “Advances in Homotopy Type Theory.”
Abstract We introduce a new method for precisely relating algebraic structures in a presheaf category and judgements of its internal type theory. The method provides a systematic way to organise …
Abstract We introduce a new method for precisely relating algebraic structures in a presheaf category and judgements of its internal type theory. The method provides a systematic way to organise complex diagrammatic reasoning and generalises the well-known Kripke-Joyal forcing for logic. As an application, we prove several properties of algebraic weak factorisation systems considered in Homotopy Type Theory.
We develop further the theory of monoidal bicategories by introducing and studying bicate- gorical counterparts of the notions of a linear explonential comonad, as considered in the study of linear …
We develop further the theory of monoidal bicategories by introducing and studying bicate- gorical counterparts of the notions of a linear explonential comonad, as considered in the study of linear logic, and of a codereliction transformation, introduced to study differential linear logic via differential categories. As an application, we extend the differential calculus of Joyal's analytic functors to analytic functors between presheaf categories, just as ordinary calculus extends from a single variable to many variables.
We extend the arithmetic product of species of structures and symmetric sequences studied by Maia and Méndez and by Dwyer and Hess to coloured symmetric sequences and show that it …
We extend the arithmetic product of species of structures and symmetric sequences studied by Maia and Méndez and by Dwyer and Hess to coloured symmetric sequences and show that it determines a normal oplax monoidal structure on the bicategory of coloured symmetric sequences. In order to do this, we establish general results on extending monoidal structures to Kleisli bicategories. Our approach uses monoidal double categories, which help us to attack the difficult problem of verifying the coherence conditions for a monoidal bicategory in an efficient way.
We provide a partial solution to the problem of defining a constructive version of Voevodsky's simplicial model of Univalent Foundations. For this, we prove constructive counterparts of the necessary results …
We provide a partial solution to the problem of defining a constructive version of Voevodsky's simplicial model of Univalent Foundations. For this, we prove constructive counterparts of the necessary results of simplicial homotopy theory, building on the constructive version of the Kan-Quillen model structure established by the second-named author. In particular, we show that dependent products along fibrations with cofibrant domains preserve fibrations, establish the weak equivalence extension property for weak equivalences between fibrations with cofibrant domain and define a univalent fibration that classifies small fibrations between bifibrant objects. These results allow us to define a comprehension category supporting identity types, Σ $\Sigma$ -types, Π $\Pi$ -types and a univalent universe, leaving only a coherence question to be addressed.
We extend the arithmetic product of species of structures and symmetric sequences studied by Maia and Mendez and by Dwyer and Hess to coloured symmetric sequences and show that it …
We extend the arithmetic product of species of structures and symmetric sequences studied by Maia and Mendez and by Dwyer and Hess to coloured symmetric sequences and show that it determines a normal oplax monoidal structure on the bicategory of coloured symmetric sequences. In order to do this, we establish general results on extending monoidal structures to Kleisli bicategories. Our approach uses monoidal double categories, which help us to attack the difficult problem of verifying the coherence conditions for a monoidal bicategory in an efficient way.
Abstract For a category $\mathcal {E}$ with finite limits and well-behaved countable coproducts, we construct a model structure, called the effective model structure, on the category of simplicial objects in …
Abstract For a category $\mathcal {E}$ with finite limits and well-behaved countable coproducts, we construct a model structure, called the effective model structure, on the category of simplicial objects in $\mathcal {E}$ , generalising the Kan–Quillen model structure on simplicial sets. We then prove that the effective model structure is left and right proper and satisfies descent in the sense of Rezk. As a consequence, we obtain that the associated $\infty $ -category has finite limits, colimits satisfying descent, and is locally Cartesian closed when $\mathcal {E}$ is but is not a higher topos in general. We also characterise the $\infty $ -category presented by the effective model structure, showing that it is the full sub-category of presheaves on $\mathcal {E}$ spanned by Kan complexes in $\mathcal {E}$ , a result that suggests a close analogy with the theory of exact completions.
Abstract We present two new proofs of Simon Henry’s result that the category of simplicial sets admits a constructive counterpart of the classical Kan–Quillen model structure. Our proofs are entirely …
Abstract We present two new proofs of Simon Henry’s result that the category of simplicial sets admits a constructive counterpart of the classical Kan–Quillen model structure. Our proofs are entirely self-contained and avoid complex combinatorial arguments on anodyne extensions. We also give new constructive proofs of the left and right properness of the model structure.
We introduce type-theoretic algebraic weak factorisation systems and show how they give rise to homotopy-theoretic models of Martin-L\"of type theory. This is done by showing that the comprehension category associated …
We introduce type-theoretic algebraic weak factorisation systems and show how they give rise to homotopy-theoretic models of Martin-L\"of type theory. This is done by showing that the comprehension category associated to a type-theoretic algebraic weak factorisation system satisfies the assumptions necessary to apply a right adjoint method for splitting comprehension categories. We then provide methods for constructing several examples of type-theoretic algebraic weak factorisation systems, encompassing the existing groupoid model and cubical sets models, as well as some models based on normal fibrations
For a category $\mathcal E$ with finite limits and well-behaved countable coproducts, we construct a model structure, called the effective model structure, on the category of simplicial objects in $\mathcal …
For a category $\mathcal E$ with finite limits and well-behaved countable coproducts, we construct a model structure, called the effective model structure, on the category of simplicial objects in $\mathcal E$, generalising the Kan--Quillen model structure on simplicial sets. We then prove that the effective model structure is left and right proper and satisfies descent in the sense of Rezk. As a consequence, we obtain that the associated $\infty$-category has finite limits, colimits satisfying descent, and is locally Cartesian closed when $\mathcal E$ is, but is not a higher topos in general. We also characterise the $\infty$-category presented by the effective model structure, showing that it is the full sub-category of presheaves on $\mathcal E$ spanned by Kan complexes in $\mathcal E$, a result that suggests a close analogy with the theory of exact completions.
We introduce a new method for precisely relating certain kinds of algebraic structures in a presheaf category and judgements of its internal type theory. The method provides a systematic way …
We introduce a new method for precisely relating certain kinds of algebraic structures in a presheaf category and judgements of its internal type theory. The method provides a systematic way to organise complex diagrammatic reasoning and generalises the well-known Kripke-Joyal forcing for logic. As an application, we prove several properties of algebraic weak factorisation systems considered in Homotopy Type Theory.
We present two new proofs of Simon Henry's result that the category of simplicial sets admits a constructive counterpart of the classical Kan-Quillen model structure. Our proofs are entirely self-contained …
We present two new proofs of Simon Henry's result that the category of simplicial sets admits a constructive counterpart of the classical Kan-Quillen model structure. Our proofs are entirely self-contained and avoid complex combinatorial arguments on anodyne extensions. We also give new constructive proofs of the left and right properness of the model structure.
We introduce type-theoretic algebraic weak factorisation systems and show how they give rise to homotopy-theoretic models of Martin-Lof type theory. This is done by showing that the comprehension category associated …
We introduce type-theoretic algebraic weak factorisation systems and show how they give rise to homotopy-theoretic models of Martin-Lof type theory. This is done by showing that the comprehension category associated to a type-theoretic algebraic weak factorisation system satisfies the assumptions necessary to apply a right adjoint method for splitting comprehension categories. We then provide methods for constructing several examples of type-theoretic algebraic weak factorisation systems, encompassing the existing groupoid model and cubical sets models, as well as some models based on normal fibrations
We introduce the notion of a relative pseudomonad, which generalizes the notion of a pseudomonad, and define the Kleisli bicategory associated to a relative pseudomonad. We then present an efficient …
We introduce the notion of a relative pseudomonad, which generalizes the notion of a pseudomonad, and define the Kleisli bicategory associated to a relative pseudomonad. We then present an efficient method to define pseudomonads on the Kleisli bicategory of a relative pseudomonad. The results are applied to define several pseudomonads on the bicategory of profunctors in an homogeneous way and provide a uniform approach to the definition of bicategories that are of interest in operad theory, mathematical logic, and theoretical computer science.
We develop further the theory of operads and analytic functors.In particular, we introduce the bicategory OpdBim V of operad bimodules, that has operads as 0-cells, operad bimodules as 1-cells and …
We develop further the theory of operads and analytic functors.In particular, we introduce the bicategory OpdBim V of operad bimodules, that has operads as 0-cells, operad bimodules as 1-cells and operad bimodule maps as 2-cells, and prove that it is cartesian closed.In order to obtain this result, we extend the theory of distributors and the formal theory of monads.
We develop further the theory of weak factorization systems and algebraic weak factorization systems. In particular, we give a method for constructing (algebraic) weak factorization systems whose right maps can …
We develop further the theory of weak factorization systems and algebraic weak factorization systems. In particular, we give a method for constructing (algebraic) weak factorization systems whose right maps can be thought of as (uniform) fibrations and that satisfy the (functorial) Frobenius condition. As applications, we obtain a new proof that the Quillen model structure for Kan complexes is right proper, avoiding entirely the use of topological realization and minimal fibrations, and we solve an open problem in the study of Voevodsky's simplicial model of type theory, proving a constructive version of the preservation of Kan fibrations by pushforward along Kan fibrations. Our results also subsume and extend work by Coquand and others on cubical sets.
We investigate inductive types in type theory, using the insights provided by homotopy type theory and univalent foundations of mathematics. We do so by introducing the new notion of a …
We investigate inductive types in type theory, using the insights provided by homotopy type theory and univalent foundations of mathematics. We do so by introducing the new notion of a homotopy-initial algebra. This notion is defined by a purely type-theoretic contractibility condition that replaces the standard, category-theoretic universal property involving the existence and uniqueness of appropriate morphisms. Our main result characterizes the types that are equivalent to W-types as homotopy-initial algebras.
We introduce and study the notion of a uniform fibration in categories with a functorial cylinder. In particular, we show that in a wide class of presheaf categories, including simplicial …
We introduce and study the notion of a uniform fibration in categories with a functorial cylinder. In particular, we show that in a wide class of presheaf categories, including simplicial sets and cubical sets with connections, uniform fibrations are the right class of a natural weak factorization system and satisfy the Frobenius condition. This implies that pushforward along a uniform fibration preserves uniform fibrations. When instantiated in simplicial sets, this result gives a constructive counterpart of one of the key facts underpinning Voevodsky's simplicial model of univalent foundations, while in cubical sets it extends some of the existing work on cubical models of type theory by Coquand and others.
We investigate inductive types in type theory, using the insights provided by homotopy type theory and univalent foundations of mathematics. We do so by introducing the new notion of a …
We investigate inductive types in type theory, using the insights provided by homotopy type theory and univalent foundations of mathematics. We do so by introducing the new notion of a homotopy-initial algebra. This notion is defined by a purely type-theoretic contractibility condition which replaces the standard, category-theoretic universal property involving the existence and uniqueness of appropriate morphisms. Our main result characterises the types that are equivalent to W-types as homotopy-initial algebras.
We give an overview of the main ideas involved in the development of homotopy type theory and the univalent foundations of Mathematics programme. This serves as a background for the …
We give an overview of the main ideas involved in the development of homotopy type theory and the univalent foundations of Mathematics programme. This serves as a background for the research papers published in the special issue.
We investigate inductive types in type theory, using the insights provided by homotopy type theory and univalent foundations of mathematics. We do so by introducing the new notion of a …
We investigate inductive types in type theory, using the insights provided by homotopy type theory and univalent foundations of mathematics. We do so by introducing the new notion of a homotopy-initial algebra. This notion is defined by a purely type-theoretic contractibility condition which replaces the standard, category-theoretic universal property involving the existence and uniqueness of appropriate morphisms. Our main result characterises the types that are equivalent to W-types as homotopy-initial algebras.
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 study polynomial functors over locally cartesian closed categories. After setting up the basic theory, we show how polynomial functors assemble into a double category, in fact a framed bicategory. …
We study polynomial functors over locally cartesian closed categories. After setting up the basic theory, we show how polynomial functors assemble into a double category, in fact a framed bicategory. We show that the free monad on a polynomial endofunctor is polynomial. The relationship with operads and other related notions is explored.
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.
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.
We characterize double adjunctions in terms of presheaves and universal squares, and then apply these characterizations to free monads and Eilenberg--Moore objects in double categories. We improve upon our earlier …
We characterize double adjunctions in terms of presheaves and universal squares, and then apply these characterizations to free monads and Eilenberg--Moore objects in double categories. We improve upon our earlier result in Monads in Double Categories, JPAA 215:6, pages 1174-1197, 2011, to conclude: if a double category with cofolding admits the construction of free monads in its horizontal 2-category, then it also admits the construction of free monads as a double category. We also prove that a double category admits Eilenberg--Moore objects if and only if a certain parameterized presheaf is representable. Along the way, we develop parameterized presheaves on double categories and prove a double-categorical Yoneda Lemma.
Homotopy type theory is an interpretation of Martin-Löf'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-Löf'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.
We characterize double adjunctions in terms of presheaves and universal squares, and then apply these characterizations to free monads and Eilenberg--Moore objects in double categories. We improve upon our earlier …
We characterize double adjunctions in terms of presheaves and universal squares, and then apply these characterizations to free monads and Eilenberg--Moore objects in double categories. We improve upon our earlier result in "Monads in Double Categories", JPAA 215:6, pages 1174-1197, 2011, to conclude: if a double category with cofolding admits the construction of free monads in its horizontal 2-category, then it also admits the construction of free monads as a double category. We also prove that a double category admits Eilenberg--Moore objects if and only if a certain parameterized presheaf is representable. Along the way, we develop parameterized presheaves on double categories and prove a double-categorical Yoneda Lemma.
We extend the basic concepts of Street's formal theory of monads from the setting of 2-categories to that of double categories. In particular, we introduce the double category Mnd(C) of …
We extend the basic concepts of Street's formal theory of monads from the setting of 2-categories to that of double categories. In particular, we introduce the double category Mnd(C) of monads in a double category C and define what it means for a double category to admit the construction of free monads. Our main theorem shows that, under some mild conditions, a double category that is a framed bicategory admits the construction of free monads if its horizontal 2-category does. We apply this result to obtain double adjunctions which extend the adjunction between graphs and categories and the adjunction between polynomial endofunctors and polynomial monads.
We extend the basic concepts of Street's formal theory of monads from the setting of 2-categories to that of double categories. In particular, we introduce the double category Mnd(C) of …
We extend the basic concepts of Street's formal theory of monads from the setting of 2-categories to that of double categories. In particular, we introduce the double category Mnd(C) of monads in a double category C and define what it means for a double category to admit the construction of free monads. Our main theorem shows that, under some mild conditions, a double category that is a framed bicategory admits the construction of free monads if its horizontal 2-category does. We apply this result to obtain double adjunctions which extend the adjunction between graphs and categories and the adjunction between polynomial endofunctors and polynomial monads.
We present a solution to the problem of defining a counterpart in Algebraic Set Theory of the construction of internal sheaves in Topos Theory. Our approach is general in that …
We present a solution to the problem of defining a counterpart in Algebraic Set Theory of the construction of internal sheaves in Topos Theory. Our approach is general in that we consider sheaves as determined by Lawvere-Tierney coverages, rather than by Grothendieck coverages, and assume only a weakening of the axioms for small maps originally introduced by Joyal and Moerdijk, thus subsuming the existing topos-theoretic results.
We contribute to the formal theory of pseudomonads, i.e. the analogue for pseudomonads of the formal theory of monads. In particular, we solve a problem posed by Steve Lack by …
We contribute to the formal theory of pseudomonads, i.e. the analogue for pseudomonads of the formal theory of monads. In particular, we solve a problem posed by Steve Lack by proving that, for every Gray-category K, there is a Gray-category Psm(K) of pseudomonads, pseudomonad morphisms, pseudomonad transformations and pseudomonad modifications in K. We then establish a triequivalence between Psm(K) and the Gray-category of pseudomonads introduced by Marmolejo. Finally, these results are applied to give a clear account of the coherence conditions for pseudodistributive laws. 41 pages. Comments welcome.
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.
We show that the classifying category C(T) of a dependent type theory T with axioms for identity types admits a non-trivial weak factorisation system. We provide an explicit characterisation of …
We show that the classifying category C(T) of a dependent type theory T with axioms for identity types admits a non-trivial weak factorisation system. We provide an explicit characterisation of the elements of both the left class and the right class of the weak factorisation system. This characterisation is applied to relate identity types and the homotopy theory of groupoids.
The concept of generalised species of structures between small categories and, correspondingly, that of generalised analytic functor between presheaf categories are introduced. An operation of substitution for generalised species, which …
The concept of generalised species of structures between small categories and, correspondingly, that of generalised analytic functor between presheaf categories are introduced. An operation of substitution for generalised species, which is the counterpart to the composition of generalised analytic functors, is also put forward. These definitions encompass most notions of combinatorial species considered in the literature — including of course Joyal's original notion — together with their associated substitution operation. Our first main result exhibits the substitution calculus of generalised species as arising from a Kleisli bicategory for a pseudo-comonad on profunctors. Our second main result establishes that the bicategory of generalised species of structures is cartesian closed.
We define what it means for a formal topology to be spatial, and investigate properties related to spatiality both in general and in examples.
We define what it means for a formal topology to be spatial, and investigate properties related to spatiality both in general and in examples.
Abstract This chapter introduces new kinds of models for constructive set theories based on categories of presheaves. It concentrates on categories of classes rather than sets, following the lines of …
Abstract This chapter introduces new kinds of models for constructive set theories based on categories of presheaves. It concentrates on categories of classes rather than sets, following the lines of algebraic set theory. It defines a general notion of what is a categorical model for CST, and shows that categories of presheaves provide examples of such models. To do so, it considers presheaves as functors with values in a category of classes. The models introduced are a counterpart of the presheaf models for intuitionistic set theories defined by Dana Scott in the 1980s. In this work, the author has to overcome the challenges intrinsic to dealing with generalized predicative formal systems rather than impredicative ones. An application to an independence result is discussed.
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.
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.
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.
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.
Higher-dimensional category theory is the study of n-categories, operads, braided monoidal categories, and other such exotic structures. It draws its inspiration from areas as diverse as topology, quantum algebra, mathematical …
Higher-dimensional category theory is the study of n-categories, operads, braided monoidal categories, and other such exotic structures. It draws its inspiration from areas as diverse as topology, quantum algebra, mathematical physics, logic, and theoretical computer science. The heart of this book is the language of generalized operads. This is as natural and transparent a language for higher category theory as the language of sheaves is for algebraic geometry, or vector spaces for linear algebra. It is introduced carefully, then used to give simple descriptions of a variety of higher categorical structures. In particular, one possible definition of n-category is discussed in detail, and some common aspects of other possible definitions are established. This is the first book on the subject and lays its foundations. It will appeal to both graduate students and established researchers who wish to become acquainted with this modern branch of mathematics.
This is a short overview of an experimental library of Mathematics formalized in the Coq proof assistant using the univalent interpretation of the underlying type theory of Coq. I started …
This is a short overview of an experimental library of Mathematics formalized in the Coq proof assistant using the univalent interpretation of the underlying type theory of Coq. I started to work on this library in February 2010 in order to gain experience with formalization of Mathematics in a constructive type theory based on the intuition gained from the univalent models (see Kapulkin et al. 2012).
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 .
We develop further the theory of weak factorization systems and algebraic weak factorization systems. In particular, we give a method for constructing (algebraic) weak factorization systems whose right maps can …
We develop further the theory of weak factorization systems and algebraic weak factorization systems. In particular, we give a method for constructing (algebraic) weak factorization systems whose right maps can be thought of as (uniform) fibrations and that satisfy the (functorial) Frobenius condition. As applications, we obtain a new proof that the Quillen model structure for Kan complexes is right proper, avoiding entirely the use of topological realization and minimal fibrations, and we solve an open problem in the study of Voevodsky's simplicial model of type theory, proving a constructive version of the preservation of Kan fibrations by pushforward along Kan fibrations. Our results also subsume and extend work by Coquand and others on cubical sets.
This paper presents a type theory in which it is possible to directly manipulate n-dimensional cubes (points, lines, squares, cubes, etc.) based on an interpretation of dependent type theory in …
This paper presents a type theory in which it is possible to directly manipulate n-dimensional cubes (points, lines, squares, cubes, etc.) based on an interpretation of dependent type theory in a cubical set model. This enables new ways to reason about identity types, for instance, function extensionality is directly provable in the system. Further, Voevodsky's univalence axiom is provable in this system. We also explain an extension with some higher inductive types like the circle and propositional truncation. Finally we provide semantics for this cubical type theory in a constructive meta-theory.
We present a model of type theory with dependent product, sum, and identity, in cubical sets. We describe a universe and explain how to transform an equivalence between two types …
We present a model of type theory with dependent product, sum, and
identity, in cubical sets. We describe a universe and explain how
to transform an equivalence between two types into an equality. We
also explain how to model propositional truncation and the circle.
While not expressed internally in type theory, the model is expressed in a constructive metalogic. Thus it is a step towards a computational interpretation of Voevodsky's Univalence Axiom.
This paper studies fundamental connections between profunctors (that is, distributors, or bimodules), open maps and bisimulation. In particular, it proves that a colimit preserving functor between presheaf categories (corresponding to …
This paper studies fundamental connections between profunctors (that is, distributors, or bimodules), open maps and bisimulation. In particular, it proves that a colimit preserving functor between presheaf categories (corresponding to a profunctor) preserves open maps and open map bisimulation. Consequently, the composition of profunctors preserves open maps as 2-cells. A guiding idea is the view that profunctors, and colimit preserving functors, are linear maps in a model of classical linear logic. But profunctors, and colimit preserving functors, as linear maps, are too restrictive for many applications. This leads to a study of a range of pseudo-comonads and of how non-linear maps in their co-Kleisli bicategories preserve open maps and bisimulation. The pseudo-comonads considered are based on finite colimit completion, 'lifting', and indexed families. The paper includes an appendix summarising the key results on coends, left Kan extensions and the preservation of colimits. One motivation for this work is that it provides a mathematical framework for extending domain theory and denotational semantics of programming languages to the more intricate models, languages and equivalences found in concurrent computation, but the results are likely to have more general applicability because of the ubiquitous nature of profunctors.
We give an analysis of the non-constructivity of the following basic result: if X and Y are simplicial sets and Y has the Kan extension property, then Y^X also has …
We give an analysis of the non-constructivity of the following basic result: if X and Y are simplicial sets and Y has the Kan extension property, then Y^X also has the Kan extension property. By means of Kripke countermodels we show that even simple consequences of this basic result, such as edge reversal and edge composition, are not constructively provable. We also show that our unprovability argument will have to be refined if one strengthens the usual formulation of the Kan extension property to one with explicit horn-filler operations.
Since the beginning of the modern era of algebraic topology, simplicial methods have been used systematically and effectively for both computation and basic theory. With the development of Quillen's c
Since the beginning of the modern era of algebraic topology, simplicial methods have been used systematically and effectively for both computation and basic theory. With the development of Quillen's c
The goal of this paper is to demystify the role played by the Reedy category axioms in homotopy theory. With no assumed prerequisites beyond a healthy appetite for category theoretic …
The goal of this paper is to demystify the role played by the Reedy category axioms in homotopy theory. With no assumed prerequisites beyond a healthy appetite for category theoretic arguments, we present streamlined proofs of a number of useful technical results, which are well known to folklore but di cult to nd in the literature. While the results presented here are not new, our approach to their proofs is somewhat novel. Speci cally, we reduce the much of the hard work involved to simpler computations involving weighted colimits and Leibniz (pushout-product) constructions. The general theory is developed in parallel with examples, which we use to prove that familiar formulae for homotopy limits and colimits indeed have the desired properties.
We provide a partial solution to the problem of defining a constructive version of Voevodsky's simplicial model of Univalent Foundations. For this, we prove constructive counterparts of the necessary results …
We provide a partial solution to the problem of defining a constructive version of Voevodsky's simplicial model of Univalent Foundations. For this, we prove constructive counterparts of the necessary results of simplicial homotopy theory, building on the constructive version of the Kan-Quillen model structure established by the second-named author. In particular, we show that dependent products along fibrations with cofibrant domains preserve fibrations, establish the weak equivalence extension property for weak equivalences between fibrations with cofibrant domain and define a univalent fibration that classifies small fibrations between bifibrant objects. These results allow us to define a comprehension category supporting identity types, Σ $\Sigma$ -types, Π $\Pi$ -types and a univalent universe, leaving only a coherence question to be addressed.
Cohomology groups ${H^q}(X,E)$ are defined, where X is a topological space and E is a sheaf on X with values in Kanâs category of spectra. These groups generalize the ordinary …
Cohomology groups ${H^q}(X,E)$ are defined, where X is a topological space and E is a sheaf on X with values in Kanâs category of spectra. These groups generalize the ordinary cohomology groups of X with coefficients in an abelian sheaf, as well as the generalized cohomology of X in the usual sense. The groups are defined by means of the âhomotopical algebraâ of Quillen applied to suitable categories of sheaves. The study of the homotopy category of sheaves of spectra requires an abstract homotopy theory more general than Quillenâs, and this is developed in Part I of the paper. Finally, the basic cohomological properties are proved, including a spectral sequence which generalizes the Atiyah-Hirzebruch spectral sequence (in generalized cohomology theory) and the âlocal to globalâ spectral sequence (in sheaf cohomology theory).
We define Anderson-Brown-Cisinski (ABC) cofibration categories, and construct homotopy colimits of diagrams of objects in ABC cofibration categories. Homotopy colimits for Quillen model categories are obtained as a particular case. …
We define Anderson-Brown-Cisinski (ABC) cofibration categories, and construct homotopy colimits of diagrams of objects in ABC cofibration categories. Homotopy colimits for Quillen model categories are obtained as a particular case. We attach to each ABC cofibration category a left Heller derivator. A dual theory is developed for homotopy limits in ABC fibration categories and for right Heller derivators. These constructions provide a natural framework for 'doing homotopy theory' in ABC (co)fibration categories.
We give an elementary construction of a certain class of model structures. In particular, we rederive the Kan model structure on simplicial sets without the use of topological spaces, minimal …
We give an elementary construction of a certain class of model structures. In particular, we rederive the Kan model structure on simplicial sets without the use of topological spaces, minimal complexes, or any concrete model of fibrant replacement such as Kan's Ex^infinity functor. Our argument makes crucial use of the glueing construction developed by Cohen et al. in the specific setting of certain cubical sets.
The concept of generalised species of structures between small categories and, correspondingly, that of generalised analytic functor between presheaf categories are introduced. An operation of substitution for generalised species, which …
The concept of generalised species of structures between small categories and, correspondingly, that of generalised analytic functor between presheaf categories are introduced. An operation of substitution for generalised species, which is the counterpart to the composition of generalised analytic functors, is also put forward. These definitions encompass most notions of combinatorial species considered in the literature — including of course Joyal's original notion — together with their associated substitution operation. Our first main result exhibits the substitution calculus of generalised species as arising from a Kleisli bicategory for a pseudo-comonad on profunctors. Our second main result establishes that the bicategory of generalised species of structures is cartesian closed.
Dans le cadre des categories doubles, on definit la limite double (horizontale) d'un foncteur double F: I → A et on donne un theoreme de construction pour ces limites, a …
Dans le cadre des categories doubles, on definit la limite double (horizontale) d'un foncteur double F: I → A et on donne un theoreme de construction pour ces limites, a partir des produits doubles, egalisateurs doubles et tabulateurs (la limite double d'un morphisme vertical). Les limites doubles decrivent des outils importants: par exemple, la construction de Grothendieck pour un profoncteur est son tabulateur, dans la categorie double C at des categories, foncteurs et profoncteurs. Si A est une 2-categorie, notre resultat se reduit a la construction de Street des limites ponderees [22]; si, d'autre part, I n'a que des fleches verticales, on retrouve la construction de Bastiani-Ehresmann des limites relatives aux categories doubles [2].
Cet article poursuit notre etude de la theorie generale des categories doubles faibles, en traitant des adjonctions et des monades. Une adjonction double generale, telle qu'elle apparait dans des situations …
Cet article poursuit notre etude de la theorie generale des categories doubles faibles, en traitant des adjonctions et des monades. Une adjonction double generale, telle qu'elle apparait dans des situations concretes, presente un foncteur double colax adjoint a gauche d'un foncteur double lax. Ce couple ne peut pas etre vu comme une adjonction dans une bicategorie, car les morphismes lax et colax n'en forment pas une. Mais ces adjonctions peuvent etre formalisees dans une categorie double interessante, formee des categories doubles faibles, avec les foncteurs doubles lax et colax comme fleches horizontales et verticales, et avec des cellules doubles convenables.
We present Voevodsky's construction of a model of univalent type theory in the category of simplicial sets. To this end, we first give a general technique for constructing categorical models …
We present Voevodsky's construction of a model of univalent type theory in the category of simplicial sets.
To this end, we first give a general technique for constructing categorical models of dependent type theory, using universes to obtain coherence. We then construct a (weakly) universal Kan fibration, and use it to exhibit a model in simplicial sets. Lastly, we introduce the Univalence Axiom, in several equivalent formulations, and show that it holds in our model.
As a corollary, we conclude that Martin-Lof type theory with one univalent universe (formulated in terms of contextual categories) is at least as consistent as ZFC with two inaccessible cardinals.
As an example of the categorical apparatus of pseudo algebras over 2-theories, we show that pseudo algebras over the 2-theory of categories can be viewed as pseudo double categories with …
As an example of the categorical apparatus of pseudo algebras over 2-theories, we show that pseudo algebras over the 2-theory of categories can be viewed as pseudo double categories with folding or as appropriate 2-functors into bicategories. Foldings are equivalent to connection pairs, and also to thin structures if the vertical and horizontal morphisms coincide. In a sense, the squares of a double category with folding are determined in a functorial way by the 2-cells of the horizontal 2-category. As a special case, strict 2-algebras with one object and everything invertible are crossed modules under a group.
Higher category theory is generally regarded as technical and forbidding, but part of it is considerably more tractable: the theory of infinity-categories, higher categories in which all higher morphisms are …
Higher category theory is generally regarded as technical and forbidding, but part of it is considerably more tractable: the theory of infinity-categories, higher categories in which all higher morphisms are assumed to be invertible. In Higher Topos Theory , Jacob Lurie presents the foundations of this theory, using the language of weak Kan complexes introduced by Boardman and Vogt, and shows how existing theorems in algebraic topology can be reformulated and generalized in the theory's new language. The result is a powerful theory with applications in many areas of mathematics. The book's first five chapters give an exposition of the theory of infinity-categories that emphasizes their role as a generalization of ordinary categories. Many of the fundamental ideas from classical category theory are generalized to the infinity-categorical setting, such as limits and colimits, adjoint functors, ind-objects and pro-objects, locally accessible and presentable categories, Grothendieck fibrations, presheaves, and Yoneda's lemma. A sixth chapter presents an infinity-categorical version of the theory of Grothendieck topoi, introducing the notion of an infinity-topos, an infinity-category that resembles the infinity-category of topological spaces in the sense that it satisfies certain axioms that codify some of the basic principles of algebraic topology. A seventh and final chapter presents applications that illustrate connections between the theory of higher topoi and ideas from classical topology.
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.
The goal of this paper is to demystify the role played by the Reedy category axioms in homotopy theory. With no assumed prerequisites beyond a healthy appetite for category theoretic …
The goal of this paper is to demystify the role played by the Reedy category axioms in homotopy theory. With no assumed prerequisites beyond a healthy appetite for category theoretic arguments, we present streamlined proofs of a number of useful technical results, which are well known to folklore but difficult to find in the literature. While the results presented here are not new, our approach to their proofs is somewhat novel. Specifically, we reduce the much of the hard work involved to simpler computations involving weighted colimits and Leibniz (pushout-product) constructions. The general theory is developed in parallel with examples, which we use to prove that familiar formulae for homotopy limits and colimits indeed have the desired properties.
Localization of model category structures: Summary of part 1 Local spaces and localization The localization model category for spaces Localization of model categories Existence of left Bousfield localizations Existence of …
Localization of model category structures: Summary of part 1 Local spaces and localization The localization model category for spaces Localization of model categories Existence of left Bousfield localizations Existence of right Bousfield localizations Fiberwise localization Homotopy theory in model categories: Summary of part 2 Model categories Fibrant and cofibrant approximations Simplicial model categories Ordinals, cardinals, and transfinite composition Cofibrantly generated model categories Cellular model categories Proper model categories The classifying space of a small category The Reedy model category structure Cosimplicial and simplicial resolutions Homotopy function complexes Homotopy limits in simplicial model categories Homotopy limits in general model categories Index Bibliography.