We present the first definition of strictly associative and unital ∞-category.Our proposal takes the form of a type theory whose terms describe the operations of such structures, and whose definitional …
We present the first definition of strictly associative and unital ∞-category.Our proposal takes the form of a type theory whose terms describe the operations of such structures, and whose definitional equality relation enforces desired strictness conditions.The key technical device is a new computation rule in the definitional equality of the theory, which we call insertion, defined in terms of a universal property.On terms for which it is defined, this operation "inserts" one of the arguments of a substituted coherence into the coherence itself, appropriately modifying the pasting diagram and result type, and simplifying the syntax in the process.We generate an equational theory from this reduction relation and we study its properties in detail, showing that it yields a decision procedure for equality.Expressed as a type theory, our model is well-adapted for generating and verifying efficient proofs of higher categorical statements.We illustrate this via an OCaml implementation, and give a number of examples, including a short encoding of the syllepsis, a 5-dimensional homotopy that plays an important role in the homotopy groups of spheres.
We present the first definition of strictly associative and unital $\infty$-category. Our proposal takes the form of a generalized algebraic theory, with operations that give the composition and coherence laws, …
We present the first definition of strictly associative and unital $\infty$-category. Our proposal takes the form of a generalized algebraic theory, with operations that give the composition and coherence laws, and equations encoding the strict associative and unital structure. The key technical idea of the paper is an equality generator called insertion, which can ``insert'' an argument context into the head context, simplifying the syntax of a term. The equational theory is defined by a reduction relation, and we study its properties in detail, showing that it yields a decision procedure for equality. Expressed as a type theory, our model is well-adapted for generating and verifying efficient proofs of higher categorical statements. We illustrate this via an OCaml implementation, and give a number of examples, including a short encoding of the syllepsis, a 5-dimensional homotopy that plays an important role in the homotopy groups of spheres.
We define a commutative monoid structure on the poset of left-exact localizations of a higher topos, that we call the acyclic product. Our approach is anchored in a structural analogy …
We define a commutative monoid structure on the poset of left-exact localizations of a higher topos, that we call the acyclic product. Our approach is anchored in a structural analogy between the poset of left-exact localizations of a topos and the poset of ideals of a commutative ring. The acyclic product is analogous to the product of ideals. The sequence of powers of a given left-exact localization defines a tower of localizations. We show how this recovers the towers of Goodwillie calculus in the unstable homotopical setting. We use this to describe the topoi of $n$-excisive functors as classifying $n$-nilpotent objects.
We use type-theoretic techniques to present an algebraic theory of $\infty$-categories with strict units. Starting with a known type-theoretic presentation of fully weak $\infty$-categories, in which terms denote valid operations, …
We use type-theoretic techniques to present an algebraic theory of $\infty$-categories with strict units. Starting with a known type-theoretic presentation of fully weak $\infty$-categories, in which terms denote valid operations, we extend the theory with a non-trivial definitional equality. This forces some operations to coincide strictly in any model, yielding the strict unit behaviour. We make a detailed investigation of the meta-theoretic properties of this theory. We give a reduction relation that generates definitional equality, and prove that it is confluent and terminating, thus yielding the first decision procedure for equality in a strictly-unital setting. Moreover, we show that our definitional equality relation identifies all terms in a disc context, providing a point comparison with a previously proposed definition of strictly unital $\infty$-category. We also prove a conservativity result, showing that every operation of the strictly unital theory indeed arises from a valid operation in the fully weak theory. From this, we infer that strict unitality is a property of an $\infty$-category rather than additional structure.
We revisit the work of To\"en--Vezzosi and Lurie on Grothendieck topologies, using the new tools of acyclic classes and congruences. We introduce a notion of extended Grothendieck topology on any …
We revisit the work of To\"en--Vezzosi and Lurie on Grothendieck topologies, using the new tools of acyclic classes and congruences. We introduce a notion of extended Grothendieck topology on any $\infty$-topos, and prove that the poset of extended Grothendieck topologies is isomorphic to that of topological localizations, hypercomplete localizations, Lawvere--Tierney topologies, and covering topologies (a variation on the notion of pretopology). It follows that these posets are small and have the structure of a frame. We revisit also the topological--cotopological factorization by introducing the notion of a cotopological morphism. And we revisit the notions of hypercompletion, hyperdescent, hypercoverings and hypersheaves associated to an extended Grothendieck topology. We also introduce the notion of forcing, which is a tool to compute with localizations of $\infty$-topoi.
We give a new description of computads for weak globular $\omega$-categories by giving an explicit inductive definition of the free words. This yields a new understanding of computads, and allows …
We give a new description of computads for weak globular $\omega$-categories by giving an explicit inductive definition of the free words. This yields a new understanding of computads, and allows a new definition of $\omega$-category that avoids the technology of globular operads. Our framework permits direct proofs of important results via structural induction, and we use this to give new proofs that every $\omega$-category is equivalent to a free one, and that the category of computads with generator-preserving maps is a presheaf topos, giving a direct description of the index category. We prove that our resulting definition of $\omega$-category agrees with that of Batanin and Leinster and that the induced notion of cofibrant replacement for $\omega$-categories coincides with that of Garner.
Polynomial functors are a categorical generalization of the usual notion of polynomial, which has found many applications in higher categories and type theory: those are generated by polynomials consisting a …
Polynomial functors are a categorical generalization of the usual notion of polynomial, which has found many applications in higher categories and type theory: those are generated by polynomials consisting a set of monomials built from sets of variables. They can be organized into a cartesian bicategory, which unfortunately fails to be closed for essentially two reasons, which we address here by suitably modifying the model. Firstly, a naive closure is too large to be well-defined, which can be overcome by restricting to polynomials which are finitary. Secondly, the resulting putative closure fails to properly take the 2-categorical structure in account. We advocate here that this can be addressed by considering polynomials in groupoids, instead of sets. For those, the constructions involved into composition have to be performed up to homotopy, which is conveniently handled in the setting of homotopy type theory: we use it here to formally perform the constructions required to build our cartesian bicategory, in Agda. Notably, this requires us introducing an axiomatization in a small universe of the type of finite types, as an appropriate higher inductive type of natural numbers and bijections.
Many definitions of weak and strict $\infty$-categories have been proposed. In this paper we present a definition for $\infty$-categories with strict associators, but which is otherwise fully weak. Our approach …
Many definitions of weak and strict $\infty$-categories have been proposed. In this paper we present a definition for $\infty$-categories with strict associators, but which is otherwise fully weak. Our approach is based on the existing type theory Catt, whose models are known to correspond to weak $\infty$-categories. We add a definitional equality relation to this theory which identifies terms with the same associativity structure, yielding a new type theory Catt$_{sa}$, for strictly associative $\infty$-categories. We also provide a reduction relation which generates definitional equality, and show it is confluent and terminating, giving an algorithm for deciding equality of terms, and making typechecking decidable.
Our key contribution, on which our reduction is based, is an operation on terms which we call insertion. This has a direct geometrical interpretation, allowing a subterm to be inserted into the head of the term, flatting its syntactic structure. We describe this operation combinatorially in terms of pasting diagrams, and also show can be characterized as a pushout of contexts. This allows reasoning about insertion using just its universal property.
We study the dependent type theory CaTT, introduced by Finster and Mimram, which presents the theory of weak $\omega$-categories, following the idea that type theories can be considered as presentations …
We study the dependent type theory CaTT, introduced by Finster and Mimram, which presents the theory of weak $\omega$-categories, following the idea that type theories can be considered as presentations of generalized algebraic theories. Our main contribution is a formal proof that the models of this type theory correspond precisely to weak $\omega$-categories, as defined by Maltsiniotis, by generalizing a definition proposed by Grothendieck for weak $\omega$-groupoids: Those are defined as suitable presheaves over a cat-coherator, which is a category encoding structure expected to be found in an $\omega$-category. This comparison is established by proving the initiality conjecture for the type theory CaTT, in a way which suggests the possible generalization to a nerve theorem for a certain class of dependent type theories
By extending type theory with a universe of definitionally associative and unital polynomial monads, we show how to arrive at a definition of opetopic type which is able to encode …
By extending type theory with a universe of definitionally associative and unital polynomial monads, we show how to arrive at a definition of opetopic type which is able to encode a number of fully coherent algebraic structures. In particular, our approach leads to a definition of ∞-groupoid internal to type theory and we prove that the type of such ∞-groupoids is equivalent to the universe of types. That is, every type admits the structure of an ∞-groupoid internally, and this structure is unique.
By extending type theory with a universe of definitionally associative and unital polynomial monads, we show how to arrive at a definition of opetopic type which is able to encode …
By extending type theory with a universe of definitionally associative and unital polynomial monads, we show how to arrive at a definition of opetopic type which is able to encode a number of fully coherent algebraic structures. In particular, our approach leads to a definition of ∞-groupoid internal to type theory and we prove that the type of such ∞-groupoids is equivalent to the universe of types. That is, every type admits the structure of an ∞-groupoid internally, and this structure is unique.
We propose a definition of higher sheaf with respect to an arbitrary set of maps $\Sigma$ in an $\infty$-topos $\mathcal{E}$. We then show that the associated reflection $\mathcal{E} \to {\rm …
We propose a definition of higher sheaf with respect to an arbitrary set of maps $\Sigma$ in an $\infty$-topos $\mathcal{E}$. We then show that the associated reflection $\mathcal{E} \to {\rm Sh}(\mathcal{E},\Sigma)$ is left-exact so that the subcategory of sheaves with respect to $\Sigma$ is itself an $\infty$-topos. Furthermore, we show that the reflection $\mathcal{E} \to {\rm Sh}(\mathcal{E},\Sigma)$ may be characterized as the left-exact localization generated by $\Sigma$. In the course of the proof, we study the interaction of various types of factorization systems, and make essential use of the notion of a \emph{modality}, that is, a factorization system whose left class is stable by base change.
We extend Homotopy Type Theory with a novel modality that is simultaneously a monad and a comonad. Because this modality induces a non-trivial endomap on every type, it requires a …
We extend Homotopy Type Theory with a novel modality that is simultaneously a monad and a comonad. Because this modality induces a non-trivial endomap on every type, it requires a more intricate judgemental structure than previous modal extensions of Homotopy Type Theory. We use this theory to develop an synthetic approach to spectra, where spectra are represented by certain types, and constructions on them by type structure: maps of spectra by ordinary functions, loop spaces by the identity type, and so on. We augment the type theory with a pair of axioms, one which implies that the spectra are stable, and the other which relates synthetic spectra to the ordinary definition of spectra in type theory as $Ω$-spectra. Finally, we show that the type theory is sound and complete for an abstract categorical semantics, in terms of a category-with-families with a weak endomorphism whose functor on contexts is a bireflection, i.e. has a counit an a unit that are a section-retraction pair.
By extending type theory with a universe of definitionally associative and unital polynomial monads, we show how to arrive at a definition of opetopic type which is able to encode …
By extending type theory with a universe of definitionally associative and unital polynomial monads, we show how to arrive at a definition of opetopic type which is able to encode a number of fully coherent algebraic structures. In particular, our approach leads to a definition of $\infty$-groupoid internal to type theory and we prove that the type of such $\infty$-groupoids is equivalent to the universe of types. That is, every type admits the structure of an $\infty$-groupoid internally, and this structure is unique.
Many definitions of weak and strict $\infty$-categories have been proposed. In this paper we present a definition for $\infty$-categories with strict associators, but which is otherwise fully weak. Our approach …
Many definitions of weak and strict $\infty$-categories have been proposed. In this paper we present a definition for $\infty$-categories with strict associators, but which is otherwise fully weak. Our approach is based on the existing type theory Catt, whose models are known to correspond to weak $\infty$-categories. We add a definitional equality relation to this theory which identifies terms with the same associativity structure, yielding a new type theory Catt$_{sa}$, for strictly associative $\infty$-categories. We also provide a reduction relation which generates definitional equality, and show it is confluent and terminating, giving an algorithm for deciding equality of terms, and making typechecking decidable. Our key contribution, on which our reduction is based, is an operation on terms which we call insertion. This has a direct geometrical interpretation, allowing a subterm to be inserted into the head of the term, flatting its syntactic structure. We describe this operation combinatorially in terms of pasting diagrams, and also show can be characterized as a pushout of contexts. This allows reasoning about insertion using just its universal property.
We study the dependent type theory CaTT, introduced by Finster and Mimram, which presents the theory of weak $\omega$-categories, following the idea that type theories can be considered as presentations …
We study the dependent type theory CaTT, introduced by Finster and Mimram, which presents the theory of weak $\omega$-categories, following the idea that type theories can be considered as presentations of generalized algebraic theories. Our main contribution is a formal proof that the models of this type theory correspond precisely to weak $\omega$-categories, as defined by Maltsiniotis, by generalizing a definition proposed by Grothendieck for weak $\omega$-groupoids: Those are defined as suitable presheaves over a cat-coherator, which is a category encoding structure expected to be found in an $\omega$-category. This comparison is established by proving the initiality conjecture for the type theory CaTT, in a way which suggests the possible generalization to a nerve theorem for a certain class of dependent type theories
We prove a generalization of the classical connectivity theorem of Blakers–Massey, valid in an arbitrary higher topos and with respect to an arbitrary modality, that is, a factorization system ( …
We prove a generalization of the classical connectivity theorem of Blakers–Massey, valid in an arbitrary higher topos and with respect to an arbitrary modality, that is, a factorization system ( L , R ) in which the left class is stable by base change. We explain how to rederive the classical result, as well as the recent generalization of Chachólski, Scherer and Werndli (Ann. Inst. Fourier 66 (2016) 2641–2665). Our proof is inspired by the one given in homotopy-type theory in Favonia et al. (2016).
We develop an approach to Goodwillie's calculus of functors using the techniques of higher topos theory. Central to our method is the introduction of the notion of fiberwise orthogonality, a …
We develop an approach to Goodwillie's calculus of functors using the techniques of higher topos theory. Central to our method is the introduction of the notion of fiberwise orthogonality, a strengthening of ordinary orthogonality which allows us to give a number of useful characterizations of the class of n-excisive maps. We use these results to show that the pushout product of a P n -equivalence with a P m -equivalence is a P m + n + 1 -equivalence. Building on topos-theoretic methods developed in previous work, we then prove a Blakers–Massey type theorem for the Goodwillie tower of functors. We show how to use the resulting techniques to rederive some foundational theorems in the subject, such as delooping of homogeneous functors.
We introduce a dependent type theory whose models are weak ω-categories, generalizing Brunerie's definition of ω-groupoids. Our type theory is based on the definition of ω-categories given by Maltsiniotis, himself …
We introduce a dependent type theory whose models are weak ω-categories, generalizing Brunerie's definition of ω-groupoids. Our type theory is based on the definition of ω-categories given by Maltsiniotis, himself inspired by Grothendieck's approach to the definition of ω-groupoids. In this setup, ω-categories are defined as presheaves preserving globular colimits over a certain category, called a coherator. The coherator encodes all operations required to be present in an ω-category: both the compositions of pasting schemes as well as their coherences. Our main contribution is to provide a canonical type-theoretical characterization of pasting schemes as contexts which can be derived from inference rules. Finally, we present an implementation of a corresponding proof system.
We introduce a dependent type theory whose models are weak {\omega}-categories, generalizing Brunerie's definition of {\omega}-groupoids. Our type theory is based on the definition of {\omega}-categories given by Maltsiniotis, himself …
We introduce a dependent type theory whose models are weak {\omega}-categories, generalizing Brunerie's definition of {\omega}-groupoids. Our type theory is based on the definition of {\omega}-categories given by Maltsiniotis, himself inspired by Grothendieck's approach to the definition of {\omega}-groupoids. In this setup, {\omega}-categories are defined as presheaves preserving globular colimits over a certain category, called a coherator. The coherator encodes all operations required to be present in an {\omega}-category: both the compositions of pasting schemes as well as their coherences. Our main contribution is to provide a canonical type-theoretical characterization of pasting schemes as contexts which can be derived from inference rules. Finally, we present an implementation of a corresponding proof system.
This paper contributes to recent investigations of the use of homotopy type theory to give machine-checked proofs of constructions from homotopy theory. We present a mechanized proof of a result …
This paper contributes to recent investigations of the use of homotopy type theory to give machine-checked proofs of constructions from homotopy theory. We present a mechanized proof of a result called the Blakers-Massey connectivity theorem, which relates the higher-dimensional loop structures of two spaces sharing a common part (represented by a pushout type, which is a generalization of a disjoint sum type) to those of the common part itself. This theorem gives important information about the pushout type, and has a number of useful corollaries, including the Freudenthal suspension theorem, which was used in previous formalizations. The proof is more direct than existing ones that apply in general category-theoretic settings for homotopy theory, and its mechanization is concise and high-level, due to novel combinations of ideas from homotopy theory and from type theory.
This paper continues investigations in "synthetic homotopy theory": the use of homotopy type theory to give machine-checked proofs of constructions from homotopy theory We present a mechanized proof of the …
This paper continues investigations in "synthetic homotopy theory": the use of homotopy type theory to give machine-checked proofs of constructions from homotopy theory We present a mechanized proof of the Blakers-Massey connectivity theorem, a result relating the higher-dimensional homotopy groups of a pushout type (roughly, a space constructed by gluing two spaces along a shared subspace) to those of the components of the pushout. This theorem gives important information about the pushout type, and has a number of useful corollaries, including the Freudenthal suspension theorem, which has been studied in previous formalizations. The new proof is more elementary than existing ones in abstract homotopy-theoretic settings, and the mechanization is concise and high-level, thanks to novel combinations of ideas from homotopy theory and type theory.
Homotopy type theory is an extension of Martin-Löf type theory with principles inspired by category theory and homotopy theory. With these extensions, type theory can be used to construct proofs …
Homotopy type theory is an extension of Martin-Löf type theory with principles inspired by category theory and homotopy theory. With these extensions, type theory can be used to construct proofs of homotopy-theoretic theorems, in a way that is very amenable to computer-checked proofs in proof assistants such as Coq and Agda. In this paper, we give a computer-checked construction of Eilenberg-MacLane spaces. For an abelian group G, an Eilenberg-MacLane space K(G,n) is a space (type) whose nth homotopy group is G, and whose homotopy groups are trivial otherwise. These spaces are a basic tool in algebraic topology; for example, they can be used to build spaces with specified homotopy groups, and to define the notion of cohomology with coefficients in G. Their construction in type theory is an illustrative example, which ties together many of the constructions and methods that have been used in homotopy type theory so far.
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 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.
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 prove a generalization of the classical connectivity theorem of Blakers–Massey, valid in an arbitrary higher topos and with respect to an arbitrary modality, that is, a factorization system ( …
We prove a generalization of the classical connectivity theorem of Blakers–Massey, valid in an arbitrary higher topos and with respect to an arbitrary modality, that is, a factorization system ( L , R ) in which the left class is stable by base change. We explain how to rederive the classical result, as well as the recent generalization of Chachólski, Scherer and Werndli (Ann. Inst. Fourier 66 (2016) 2641–2665). Our proof is inspired by the one given in homotopy-type theory in Favonia et al. (2016).
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.
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 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.
The aim of this paper is to present a simplified version of the notion of $\infty$-groupoid developed by Grothendieck in Pursuing Stacks and to introduce a definition of $\infty$-categories inspired …
The aim of this paper is to present a simplified version of the notion of $\infty$-groupoid developed by Grothendieck in Pursuing Stacks and to introduce a definition of $\infty$-categories inspired by Grothendieck's approach.
We develop an approach to Goodwillie's calculus of functors using the techniques of higher topos theory. Central to our method is the introduction of the notion of fiberwise orthogonality, a …
We develop an approach to Goodwillie's calculus of functors using the techniques of higher topos theory. Central to our method is the introduction of the notion of fiberwise orthogonality, a strengthening of ordinary orthogonality which allows us to give a number of useful characterizations of the class of n-excisive maps. We use these results to show that the pushout product of a P n -equivalence with a P m -equivalence is a P m + n + 1 -equivalence. Building on topos-theoretic methods developed in previous work, we then prove a Blakers–Massey type theorem for the Goodwillie tower of functors. We show how to use the resulting techniques to rederive some foundational theorems in the subject, such as delooping of homogeneous functors.
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.
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.
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 Eckmann-Hilton argument shows that any two monoid structures on the same set satisfying the interchange law are in fact the same operation, which is moreover commutative. When the monoids …
The Eckmann-Hilton argument shows that any two monoid structures on the same set satisfying the interchange law are in fact the same operation, which is moreover commutative. When the monoids correspond to the vertical and horizontal composition of a sufficiently higher-dimensional category, the Eckmann-Hilton argument itself appears as a higher cell. This cell is often required to satisfy an additional piece of coherence, which is known as the syllepsis. We show that the syllepsis can be constructed from the elimination rule of intensional identity types in Martin-Löf type theory.
Abstract We develop an $\infty $-categorical version of the classical theory of polynomial and analytic functors, initial algebras, and free monads. Using this machinery, we provide a new model for …
Abstract We develop an $\infty $-categorical version of the classical theory of polynomial and analytic functors, initial algebras, and free monads. Using this machinery, we provide a new model for $\infty $-operads, namely $\infty $-operads as analytic monads. We justify this definition by proving that the $\infty $-category of analytic monads is equivalent to that of dendroidal Segal spaces, known to be equivalent to the other existing models for $\infty $-operads.
We present a variant of the small object argument, inspired by Kelly, better suited to construct unique factorisation systems. Our main result is to compare it to the plus-construction involved …
We present a variant of the small object argument, inspired by Kelly, better suited to construct unique factorisation systems. Our main result is to compare it to the plus-construction involved in sheafification. We apply this to construct localizations, modalities and left-exact localizations explicitly from generators.
We describe a homotopical version of the relational and gluing models of type theory, and generalize it to inverse diagrams and oplax limits. Our method uses the Reedy homotopy theory …
We describe a homotopical version of the relational and gluing models of type theory, and generalize it to inverse diagrams and oplax limits. Our method uses the Reedy homotopy theory on inverse diagrams, and relies on the fact that Reedy fibrant diagrams correspond to contexts of a certain shape in type theory. This has two main applications. First, by considering inverse diagrams in Voevodsky's univalent model in simplicial sets, we obtain new models of univalence in a number of (∞, 1)-toposes; this answers a question raised at the Oberwolfach workshop on homotopical type theory. Second, by gluing the syntactic category of univalent type theory along its global sections functor to groupoids, we obtain a partial answer to Voevodsky's homotopy-canonicity conjecture: in 1-truncated type theory with one univalent universe of sets, any closed term of natural number type is homotopic to a numeral.
Homotopy type theory is an extension of Martin-Löf type theory with principles inspired by category theory and homotopy theory. With these extensions, type theory can be used to construct proofs …
Homotopy type theory is an extension of Martin-Löf type theory with principles inspired by category theory and homotopy theory. With these extensions, type theory can be used to construct proofs of homotopy-theoretic theorems, in a way that is very amenable to computer-checked proofs in proof assistants such as Coq and Agda. In this paper, we give a computer-checked construction of Eilenberg-MacLane spaces. For an abelian group G, an Eilenberg-MacLane space K(G,n) is a space (type) whose nth homotopy group is G, and whose homotopy groups are trivial otherwise. These spaces are a basic tool in algebraic topology; for example, they can be used to build spaces with specified homotopy groups, and to define the notion of cohomology with coefficients in G. Their construction in type theory is an illustrative example, which ties together many of the constructions and methods that have been used in homotopy type theory so far.
We use type-theoretic techniques to present an algebraic theory of $\infty$-categories with strict units. Starting with a known type-theoretic presentation of fully weak $\infty$-categories, in which terms denote valid operations, …
We use type-theoretic techniques to present an algebraic theory of $\infty$-categories with strict units. Starting with a known type-theoretic presentation of fully weak $\infty$-categories, in which terms denote valid operations, we extend the theory with a non-trivial definitional equality. This forces some operations to coincide strictly in any model, yielding the strict unit behaviour. We make a detailed investigation of the meta-theoretic properties of this theory. We give a reduction relation that generates definitional equality, and prove that it is confluent and terminating, thus yielding the first decision procedure for equality in a strictly-unital setting. Moreover, we show that our definitional equality relation identifies all terms in a disc context, providing a point comparison with a previously proposed definition of strictly unital $\infty$-category. We also prove a conservativity result, showing that every operation of the strictly unital theory indeed arises from a valid operation in the fully weak theory. From this, we infer that strict unitality is a property of an $\infty$-category rather than additional structure.
In this paper, we present a directed homotopy type theory for reasoning synthetically about (higher) categories and directed homotopy theory. We specify a new 'homomorphism' type former for Martin-Löf type …
In this paper, we present a directed homotopy type theory for reasoning synthetically about (higher) categories and directed homotopy theory. We specify a new 'homomorphism' type former for Martin-Löf type theory which is roughly analogous to the identity type former originally introduced by Martin-Löf. The homomorphism type former is meant to capture the notions of morphism (from the theory of categories) and directed path (from directed homotopy theory) just as the identity type former is known to capture the notions of isomorphism (from the theory of groupoids) and path (from homotopy theory). Our main result is an interpretation of these homomorphism types into Cat, the category of small categories. There, the interpretation of each homomorphism type homC(a,b) is indeed the set of morphisms between the objects a and b of the category C. We end the paper with an analysis of the interpretation in Cat with which we argue that our homomorphism types are indeed the directed version of Martin-Löf's identity types
Univalent homotopy type theory (HoTT) may be seen as a language for the category of $\infty$-groupoids. It is being developed as a new foundation for mathematics and as an internal …
Univalent homotopy type theory (HoTT) may be seen as a language for the
category of $\infty$-groupoids. It is being developed as a new foundation for
mathematics and as an internal language for (elementary) higher toposes. We
develop the theory of factorization systems, reflective subuniverses, and
modalities in homotopy type theory, including their construction using a
localization higher inductive type. This produces in particular the
($n$-connected, $n$-truncated) factorization system as well as internal
presentations of subtoposes, through lex modalities. We also develop the
semantics of these constructions.
We develop category theory within Univalent Foundations, which is a foundational system for mathematics based on a homotopical interpretation of dependent type theory. In this system, we propose a definition …
We develop category theory within Univalent Foundations, which is a foundational system for mathematics based on a homotopical interpretation of dependent type theory. In this system, we propose a definition of ‘category’ for which equality and equivalence of categories agree. Such categories satisfy a version of the univalence axiom, saying that the type of isomorphisms between any two objects is equivalent to the identity type between these objects; we call them ‘saturated’ or ‘univalent’ categories. Moreover, we show that any category is weakly equivalent to a univalent one in a universal way. In homotopical and higher-categorical semantics, this construction corresponds to a truncated version of the Rezk completion for Segal spaces, and also to the stack completion of a prestack.
We look at strict $n$-groupoids and show that if $\Re$ is any realization functor from the category of strict $n$-groupoids to the category of spaces satisfying a minimal property of …
We look at strict $n$-groupoids and show that if $\Re$ is any realization functor from the category of strict $n$-groupoids to the category of spaces satisfying a minimal property of compatibility with homotopy groups, then there is no strict $n$-groupoid $G$ such that $\Re (G)$ is the $n$-type of $S^2$ (for $n\geq 3$). At the end we speculate on how one might fix this problem by introducing a notion of ``snucategory'', a strictly associative $n$-category with only weak units.
We construct a new model category presenting the homotopy theory of presheaves on EI $(\infty,1)$-categories, which contains universe objects that satisfy Voevodsky's univalence axiom. In addition to diagrams on ordinary …
We construct a new model category presenting the homotopy theory of presheaves on EI $(\infty,1)$-categories, which contains universe objects that satisfy Voevodsky's univalence axiom. In addition to diagrams on ordinary inverse categories, as considered in previous work of the author, this includes a new model for equivariant algebraic topology with a compact Lie group of equivariance. Thus, it offers the potential for applications of homotopy type theory to equivariant homotopy theory.
Homotopy theory can be developed synthetically in homotopy type theory, using types to describe spaces, the identity type to describe paths in a space, and iterated identity types to describe …
Homotopy theory can be developed synthetically in homotopy type theory, using types to describe spaces, the identity type to describe paths in a space, and iterated identity types to describe higher-dimensional paths.While some aspects of homotopy theory have been developed synthetically and formalized in proof assistants, some seemingly easy examples have proved difficult because the required manipulations of paths becomes complicated.In this paper, we describe a cubical approach to developing homotopy theory within type theory.The identity type is complemented with higher-dimensional cube types, such as a type of squares, dependent on four points and four lines, and a type of three-dimensional cubes, dependent on the boundary of a cube.Path-over-a-path types and higher generalizations are used to describe cubes in a fibration over a cube in the base.These higher-dimensional cube and path-over types can be defined from the usual identity type, but isolating them as independent conceptual abstractions has allowed for the formalization of some previously difficult examples.
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 define and develop two-level type theory (2LTT), a version of Martin-Lof type theory which combines two different type theories. We refer to them as the inner and the outer …
We define and develop two-level type theory (2LTT), a version of Martin-Lof type theory which combines two different type theories. We refer to them as the inner and the outer type theory. In our case of interest, the inner theory is homotopy type theory (HoTT) which may include univalent universes and higher inductive types. The outer theory is a traditional form of type theory validating uniqueness of identity proofs (UIP). One point of view on it is as internalised meta-theory of the inner type theory.
There are two motivations for 2LTT. Firstly, there are certain results about HoTT which are of meta-theoretic nature, such as the statement that semisimplicial types up to level $n$ can be constructed in HoTT for any externally fixed natural number $n$. Such results cannot be expressed in HoTT itself, but they can be formalised and proved in 2LTT, where $n$ will be a variable in the outer theory. This point of view is inspired by observations about conservativity of presheaf models.
Secondly, 2LTT is a framework which is suitable for formulating additional axioms that one might want to add to HoTT. This idea is heavily inspired by Voevodsky's Homotopy Type System (HTS), which constitutes one specific instance of a 2LTT. HTS has an axiom ensuring that the type of natural numbers behaves like the external natural numbers, which allows the construction of a universe of semisimplicial types. In 2LTT, this axiom can be stated simply be asking the inner and outer natural numbers to be isomorphic.
After defining 2LTT, we set up a collection of tools with the goal of making 2LTT a convenient language for future developments. As a first such application, we develop the theory of Reedy fibrant diagrams in the style of Shulman. Continuing this line of thought, we suggest a definition of (infinity,1)-category and give some examples.
The importance of finite limits in completeness conditions has been long recognized. One has only to consider elementary toposes, pretoposes, exact categories, etc., to realize their ubiquity. However, often pullbacks …
The importance of finite limits in completeness conditions has been long recognized. One has only to consider elementary toposes, pretoposes, exact categories, etc., to realize their ubiquity. However, often pullbacks suffice and in a sense are more natural. For example it is pullbacks that are the essential ingredient in composition of spans, partial morphisms and relations. In fact the original definition of elementary topos was based on the notion of partial morphism classifier which involved only pullbacks (see [6]). Many constructions in topos theory, involving left exact functors, such as coalgebras on a cotriple and the gluing construction, also work for pullback preserving functors. And pullback preserving functors occur naturally in the subject, e.g. constant functors and the Σ α . These observations led Rosebrugh and Wood to introduce partial geometric morphisms; functors with a pullback preserving left adjoint [9]. Other reasons led Kennison independently to introduce the same concept under the name semi-geometric functors [5].
The goal of this thesis is to prove that π4(S3) ≃ Z/2Z in homotopy type theory. In particular it is a constructive and purely homotopy-theoretic proof. We first recall the …
The goal of this thesis is to prove that π4(S3) ≃ Z/2Z in homotopy type theory. In particular it is a constructive and purely homotopy-theoretic proof. We first recall the basic concepts of homotopy type theory, and we prove some well-known results about the homotopy groups of spheres: the computation of the homotopy groups of the circle, the triviality of those of the form πk(Sn) with k < n, and the construction of the Hopf fibration. We then move to more advanced tools. In particular, we define the James construction which allows us to prove the Freudenthal suspension theorem and the fact that there exists a natural number n such that π4(S3) ≃ Z/nZ. Then we study the smash product of spheres, we construct the cohomology ring of a space, and we introduce the Hopf invariant, allowing us to narrow down the n to either 1 or 2. The Hopf invariant also allows us to prove that all the groups of the form π4n−1(S2n) are infinite. Finally we construct the Gysin exact sequence, allowing us to compute the cohomology of CP2 and to prove that π4(S3) ≃ Z/2Z and that more generally πn+1(Sn) ≃ Z/2Z for every n ≥ 3
Univalent homotopy type theory (HoTT) may be seen as a language for the category of $\infty$-groupoids. It is being developed as a new foundation for mathematics and as an internal …
Univalent homotopy type theory (HoTT) may be seen as a language for the category of $\infty$-groupoids. It is being developed as a new foundation for mathematics and as an internal language for (elementary) higher toposes. We develop the theory of factorization systems, reflective subuniverses, and modalities in homotopy type theory, including their construction using a "localization" higher inductive type. This produces in particular the ($n$-connected, $n$-truncated) factorization system as well as internal presentations of subtoposes, through lex modalities. We also develop the semantics of these constructions.
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.