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 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.
This is an explanation of how cohomology is seen through the lens of n-category theory. Special topics include nonabelian cohomology, Postnikov towers, the theory of 'n-stuff', and n-categories for n …
This is an explanation of how cohomology is seen through the lens of n-category theory. Special topics include nonabelian cohomology, Postnikov towers, the theory of 'n-stuff', and n-categories for n = −1 and −2. A lengthy appendix clarifies certain puzzles and ventures into deeper waters such as higher topos theory. An annotated bibliography provides directions for further study.
In some bicategories, the 1-cells are `morphisms' between the 0-cells, such as functors between categories, but in others they are `objects' over the 0-cells, such as bimodules, spans, distributors, or …
In some bicategories, the 1-cells are `morphisms' between the 0-cells, such as functors between categories, but in others they are `objects' over the 0-cells, such as bimodules, spans, distributors, or parametrized spectra. Many bicategorical notions do not work well in these cases, because the `morphisms between 0-cells', such as ring homomorphisms, are missing. We can include them by using a pseudo double category, but usually these morphisms also induce base change functors acting on the 1-cells. We avoid complicated coherence problems by describing base change `nonalgebraically', using categorical fibrations. The resulting `framed bicategories' assemble into 2-categories, with attendant notions of equivalence, adjunction, and so on which are more appropriate for our examples than are the usual bicategorical ones.
We then describe two ways to construct framed bicategories. One is an analogue of rings and bimodules which starts from one framed bicategory and builds another. The other starts from a `monoidal fibration', meaning a parametrized family of monoidal categories, and produces an analogue of the framed bicategory of spans. Combining the two, we obtain a construction which includes both enriched and internal categories as special cases.
We present a method of constructing symmetric monoidal bicategories from symmetric monoidal double categories that satisfy a lifting condition. Such symmetric monoidal double categories frequently occur in nature, so the …
We present a method of constructing symmetric monoidal bicategories from symmetric monoidal double categories that satisfy a lifting condition. Such symmetric monoidal double categories frequently occur in nature, so the method is widely applicable, though not universally so.
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.
Higher inductive types are a class of type-forming rules, introduced to provide basic (and not-so-basic) homotopy-theoretic constructions in a type-theoretic style. They have proven very fruitful for the "synthetic" development …
Higher inductive types are a class of type-forming rules, introduced to provide basic (and not-so-basic) homotopy-theoretic constructions in a type-theoretic style. They have proven very fruitful for the "synthetic" development of homotopy theory within type theory, as well as in formalizing ordinary set-level mathematics in type theory. In this article, we construct models of a wide range of higher inductive types in a fairly wide range of settings. We introduce the notion of cell monad with parameters: a semantically-defined scheme for specifying homotopically well-behaved notions of structure. We then show that any suitable model category has *weakly stable typal initial algebras* for any cell monad with parameters. When combined with the local universes construction to obtain strict stability, this specializes to give models of specific higher inductive types, including spheres, the torus, pushout types, truncations, the James construction, and general localisations. Our results apply in any sufficiently nice Quillen model category, including any right proper, simplicially locally cartesian closed, simplicial Cisinski model category (such as simplicial sets) and any locally presentable locally cartesian closed category (such as sets) with its trivial model structure. In particular, any locally presentable locally cartesian closed $(\infty,1)$-category is presented by some model category to which our results apply.
Questions of set-theoretic size play an essential role in category theory, especially the distinction between sets and proper classes (or small sets and large sets). There are many different ways …
Questions of set-theoretic size play an essential role in category theory, especially the distinction between sets and proper classes (or small sets and large sets). There are many different ways to formalize this, and which choice is made can have noticeable effects on what categorical constructions are permissible. In this expository paper we summarize and compare a number of such "set-theoretic foundations for category theory," and describe their implications for the everyday use of category theory. We assume the reader has some basic knowledge of category theory, but little or no prior experience with formal logic or set theory.
Homotopy limits and colimits are homotopical replacements for the usual limits and colimits of category theory, which can be approached either using classical explicit constructions or the modern abstract machinery …
Homotopy limits and colimits are homotopical replacements for the usual limits and colimits of category theory, which can be approached either using classical explicit constructions or the modern abstract machinery of derived functors. Our first goal in this paper is expository: we explain both approaches and a proof of their equivalence. Our second goal is to generalize this result to enriched categories and homotopy weighted limits, showing that the classical explicit constructions still give the right answer in the abstract sense. This result partially bridges the gap between classical homotopy theory and modern abstract homotopy theory. To do this we introduce a notion of "enriched homotopical categories", which are more general than enriched model categories, but are still a good place to do enriched homotopy theory. This demonstrates that the presence of enrichment often simplifies rather than complicates matters, and goes some way toward achieving a better understanding of "the role of homotopy in homotopy theory."
We combine homotopy type theory with axiomatic cohesion, expressing the latter internally with a version of ‘adjoint logic’ in which the discretization and codiscretization modalities are characterized using a judgemental …
We combine homotopy type theory with axiomatic cohesion, expressing the latter internally with a version of ‘adjoint logic’ in which the discretization and codiscretization modalities are characterized using a judgemental formalism of ‘crisp variables.’ This yields type theories that we call ‘spatial’ and ‘cohesive,’ in which the types can be viewed as having independent topological and homotopical structure. These type theories can then be used to study formally the process by which topology gives rise to homotopy theory (the ‘fundamental ∞-groupoid’ or ‘shape’), disentangling the ‘identifications’ of homotopy type theory from the ‘continuous paths’ of topology. In a further refinement called ‘real-cohesion,’ the shape is determined by continuous maps from the real numbers, as in classical algebraic topology. This enables us to reproduce formally some of the classical applications of homotopy theory to topology. As an example, we prove Brouwer's fixed-point theorem.
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.
In some bicategories, the 1-cells are `morphisms' between the 0-cells, such as functors between categories, but in others they are `objects' over the 0-cells, such as bimodules, spans, distributors, or …
In some bicategories, the 1-cells are `morphisms' between the 0-cells, such as functors between categories, but in others they are `objects' over the 0-cells, such as bimodules, spans, distributors, or parametrized spectra. Many bicategorical notions do not work well in these cases, because the `morphisms between 0-cells', such as ring homomorphisms, are missing. We can include them by using a pseudo double category, but usually these morphisms also induce base change functors acting on the 1-cells. We avoid complicated coherence problems by describing base change `nonalgebraically', using categorical fibrations. The resulting `framed bicategories' assemble into 2-categories, with attendant notions of equivalence, adjunction, and so on which are more appropriate for our examples than are the usual bicategorical ones. We then describe two ways to construct framed bicategories. One is an analogue of rings and bimodules which starts from one framed bicategory and builds another. The other starts from a `monoidal fibration', meaning a parametrized family of monoidal categories, and produces an analogue of the framed bicategory of spans. Combining the two, we obtain a construction which includes both enriched and internal categories as special cases.
We report on the development of the HoTT library, a formalization of homotopy type theory in the Coq proof assistant. It formalizes most of basic homotopy type theory, including univalence, …
We report on the development of the HoTT library, a formalization of homotopy type theory in the Coq proof assistant. It formalizes most of basic homotopy type theory, including univalence, higher inductive types, and significant amounts of synthetic homotopy theory, as well as category theory and modalities. The library has been used as a basis for several independent developments. We discuss the decisions that led to the design of the library, and we comment on the interaction of homotopy type theory with recently introduced features of Coq, such as universe polymorphism and private inductive types.
By the Lefschetz fixed point theorem, if an endomorphism of a topological space is fixed-point-free, then its Lefschetz number vanishes. This necessary condition is not usually sufficient, however; for that …
By the Lefschetz fixed point theorem, if an endomorphism of a topological space is fixed-point-free, then its Lefschetz number vanishes. This necessary condition is not usually sufficient, however; for that we need a refinement of the Lefschetz number called the Reidemeister trace. Abstractly, the Lefschetz number is a trace in a symmetric monoidal category, while the Reidemeister trace is a trace in a bicategory; in this paper we relate these contexts using indexed symmetric monoidal categories. In particular, we will show that for any symmetric monoidal category with an associated indexed symmetric monoidal category, there is an associated bicategory which produces refinements of trace analogous to the Reidemeister trace. This bicategory also produces a new notion of trace for parametrized spaces with dualizable fibers, which refines the obvious "fiberwise" traces by incorporating the action of the fundamental group of the base space. We also advance the basic theory of indexed monoidal categories, including introducing a string diagram calculus which makes calculations much more tractable. This abstract framework lays the foundation for generalizations of these ideas to other contexts.
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 show that Voevodsky's univalence axiom for homotopy type theory is valid in categories of simplicial presheaves on elegant Reedy categories.In addition to diagrams on inverse categories, as considered in …
We show that Voevodsky's univalence axiom for homotopy type theory is valid in categories of simplicial presheaves on elegant Reedy categories.In addition to diagrams on inverse categories, as considered in previous work of the author, this includes bisimplicial sets and Θ n -spaces.This has potential applications to the study of homotopical models for higher categories.
We implement in the formal language of homotopy type theory a new set of axioms called cohesion. Then we indicate how the resulting cohesive homotopy type theory naturally serves as …
We implement in the formal language of homotopy type theory a new set of axioms called cohesion. Then we indicate how the resulting cohesive homotopy type theory naturally serves as a formal foundation for central concepts in quantum gauge field theory. This is a brief survey of work by the authors developed in detail elsewhere.
We introduce a new categorical framework for studying de- rived functors, and in particular for comparing composites of left and right derived functors. Our central observation is that model categories …
We introduce a new categorical framework for studying de- rived functors, and in particular for comparing composites of left and right derived functors. Our central observation is that model categories are the objects of a double category whose vertical and horizontal ar- rows are left and right Quillen functors, respectively, and that passage to derived functors is functorial at the level of this double category. The theory of conjunctions and mates in double categories, which generalizes the theory of adjunctions and mates in 2-categories, then gives us canon- ical ways to compare composites of left and right derived functors. We give a number of sample applications, most of which are improvements of existing proofs in the literature.
We present a method of constructing monoidal, braided monoidal, and symmetric monoidal bicategories from corresponding types of monoidal double categories that satisfy a lifting condition. Many important monoidal bicategories arise …
We present a method of constructing monoidal, braided monoidal, and symmetric monoidal bicategories from corresponding types of monoidal double categories that satisfy a lifting condition. Many important monoidal bicategories arise naturally in this way, and applying our general method is much easier than explicitly verifying the coherence laws of a monoidal bicategory for each example. Abstracting from earlier work in this direction, we express the construction as a functor between locally cubical bicategories that preserves monoid objects; this ensures that it also preserves monoidal functors, transformations, adjunctions, and so on. Examples include the monoidal bicategories of algebras and bimodules, categories and profunctors, sets and spans, open Markov processes, parametrized spectra, and various functors relating them.
We prove a general theorem which includes most notions of "exact completion". The theorem is that "k-ary exact categories" are a reflective sub-2-category of "k-ary sites", for any regular cardinal …
We prove a general theorem which includes most notions of "exact completion". The theorem is that "k-ary exact categories" are a reflective sub-2-category of "k-ary sites", for any regular cardinal k. A k-ary exact category is an exact category with disjoint and universal k-small coproducts, and a k-ary site is a site whose covering sieves are generated by k-small families and which satisfies a weak size condition. For different values of k, this includes the exact completions of a regular category or a category with (weak) finite limits; the pretopos completion of a coherent category; and the category of sheaves on a small site. For a large site with k the size of the universe, it gives a well-behaved "category of small sheaves". Along the way, we define a slightly generalized notion of "morphism of sites", and show that k-ary sites are equivalent to a type of "enhanced allegory".
Abstract Motivated by traces of matrices and Euler characteristics of topological spaces, we expect abstract traces in a symmetric monoidal category to be “additive”. When the category is “stable” in …
Abstract Motivated by traces of matrices and Euler characteristics of topological spaces, we expect abstract traces in a symmetric monoidal category to be “additive”. When the category is “stable” in some sense, additivity along cofiber sequences is a question about the interaction of stability and the monoidal structure. May proved such an additivity theorem when the stable structure is a triangulation, based on new axioms for monoidal triangulated categories. in this paper we use stable derivators instead, which are a different model for “stable homotopy theories”. We define and study monoidal structures on derivators, providing a context to describe the interplay between stability and monoidal structure using only ordinary category theory and universal properties. We can then perform May's proof of the additivity of traces in a closed monoidal stable derivator without needing extra axioms, as all the needed compatibility is automatic.
We show that in any symmetric monoidal category, if a weight for colimits is absolute, then the resulting colimit of any diagram of dualizable objects is again dualizable. Moreover, in …
We show that in any symmetric monoidal category, if a weight for colimits is absolute, then the resulting colimit of any diagram of dualizable objects is again dualizable. Moreover, in this case, if an endomorphism of the colimit is induced by an endomorphism of the diagram, then its trace can be calculated as a linear combination of traces on the objects in the diagram. The formal nature of this result makes it easy to generalize to traces in homotopical contexts (using derivators) and traces in bicategories. These generalizations include the familiar additivity of the Euler characteristic and Lefschetz number along cofiber sequences, as well as an analogous result for the Reidemeister trace, but also the orbit-counting theorem for sets with a group action, and a general formula for homotopy colimits over EI-categories.
We develop a theory of categories which are simultaneously (1) indexed over a base category S with finite products, and (2) enriched over an S-indexed monoidal category V. This includes …
We develop a theory of categories which are simultaneously (1) indexed over a base category S with finite products, and (2) enriched over an S-indexed monoidal category V. This includes classical enriched categories, indexed and fibered categories, and internal categories as special cases. We then describe the appropriate notion of "limit" for such enriched indexed categories, and show that they admit "free cocompletions" constructed as usual with a Yoneda embedding.
Notions of generalized multicategory have been defined in numerous contexts throughout the literature, and include such diverse examples as symmetric multicategories, globular operads, Lawvere theories, and topological spaces. In each …
Notions of generalized multicategory have been defined in numerous contexts throughout the literature, and include such diverse examples as symmetric multicategories, globular operads, Lawvere theories, and topological spaces. In each case, generalized multicategories are defined as the "lax algebras" or "Kleisli monoids" relative to a "monad" on a bicategory. However, the meanings of these words differ from author to author, as do the specific bicategories considered. We propose a unified framework: by working with monads on double categories and related structures (rather than bicategories), one can define generalized multicategories in a way that unifies all previous examples, while at the same time simplifying and clarifying much of the theory.
We show that stable derivators, like stable model categories, admit Mayer-Vietoris sequences arising from cocartesian squares.Along the way we characterize homotopy exact squares and give a detection result for colimiting …
We show that stable derivators, like stable model categories, admit Mayer-Vietoris sequences arising from cocartesian squares.Along the way we characterize homotopy exact squares and give a detection result for colimiting diagrams in derivators.As an application, we show that a derivator is stable if and only if its suspension functor is an equivalence.
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.
Homotopy type theory and univalent foundations (HoTT/UF) is a new foundation of mathematics, based not on set theory but on “infinity-groupoids”, which consist of collections of objects, ways in which …
Homotopy type theory and univalent foundations (HoTT/UF) is a new foundation of mathematics, based not on set theory but on “infinity-groupoids”, which consist of collections of objects, ways in which two objects can be equal, ways in which those ways-to-be-equal can be equal, ad infinitum. Though apparently complicated, such structures are increasingly important in mathematics. Philosophically, they are an inevitable result of the notion that whenever we form a collection of things, we must simultaneously consider when two of those things are the same. The “synthetic” nature of HoTT/UF enables a much simpler description of infinity groupoids than is available in set theory, thereby aligning with modern mathematics while placing “equality” back in the foundations of logic. This chapter will introduce the basic ideas of HoTT/UF for a philosophical audience, including Voevodsky’s univalence axiom and higher inductive types.
This is an introduction to type theory, synthetic topology, and homotopy type theory from a category-theoretic and topological point of view, written as a chapter for the book New Spaces …
This is an introduction to type theory, synthetic topology, and homotopy type theory from a category-theoretic and topological point of view, written as a chapter for the book New Spaces for Mathematics and Physics (ed. Gabriel Catren and Mathieu Anel).
We introduce a new categorical framework for studying derived functors, and in particular for comparing composites of left and right derived functors. Our central observation is that model categories are …
We introduce a new categorical framework for studying derived functors, and in particular for comparing composites of left and right derived functors. Our central observation is that model categories are the objects of a double category whose vertical and horizontal arrows are left and right Quillen functors, respectively, and that passage to derived functors is functorial at the level of this double category. The theory of conjunctions and mates in double categories, which generalizes the theory of adjunctions and mates in 2-categories, then gives us canonical ways to compare composites of left and right derived functors. We give a number of sample applications, most of which are improvements of existing proofs in the literature.
Magnitude is a numerical invariant of enriched categories, including in particular metric spaces as $[0,\infty)$-enriched categories. We show that in many cases magnitude can be categorified to a homology theory …
Magnitude is a numerical invariant of enriched categories, including in particular metric spaces as $[0,\infty)$-enriched categories. We show that in many cases magnitude can be categorified to a homology theory for enriched categories, which we call magnitude homology (in fact, it is a special sort of Hochschild homology), whose graded Euler characteristic is the magnitude. Magnitude homology of metric spaces generalizes the Hepworth--Willerton magnitude homology of graphs, and detects geometric information such as convexity.
We prove the conjecture that any Grothendieck $(\infty,1)$-topos can be presented by a Quillen model category that interprets homotopy type theory with strict univalent universes. Thus, homotopy type theory can …
We prove the conjecture that any Grothendieck $(\infty,1)$-topos can be presented by a Quillen model category that interprets homotopy type theory with strict univalent universes. Thus, homotopy type theory can be used as a formal language for reasoning internally to $(\infty,1)$-toposes, just as higher-order logic is used for 1-toposes. As part of the proof, we give a new, more explicit, characterization of the fibrations in injective model structures on presheaf categories. In particular, we show that they generalize the coflexible algebras of 2-monad theory.
Magnitude is a numerical invariant of enriched categories, including in particular metric spaces as [0, ∞)-enriched categories.We show that in many cases magnitude can be categorified to a homology theory …
Magnitude is a numerical invariant of enriched categories, including in particular metric spaces as [0, ∞)-enriched categories.We show that in many cases magnitude can be categorified to a homology theory for enriched categories, which we call magnitude homology (in fact, it is a special sort of Hochschild homology), whose graded Euler characteristic is the magnitude.Magnitude homology of metric spaces generalizes the Hepworth-Willerton magnitude homology of graphs, and detects geometric information such as convexity.
We extend the usual internal logic of a (pre)topos to a more general interpretation, called the stack semantics, which allows for quantifiers ranging over the class of objects of the …
We extend the usual internal logic of a (pre)topos to a more general interpretation, called the stack semantics, which allows for quantifiers ranging over the class of objects of the topos. Using well-founded relations inside the stack semantics, we can then recover a membership-based (or material) set theory from an arbitrary topos, including even set-theoretic axiom schemas such as collection and separation which involve unbounded quantifiers. This construction reproduces the models of Fourman-Hayashi and of algebraic set theory, when the latter apply. It turns out that the axioms of collection and replacement are always valid in the stack semantics of any topos, while the axiom of separation expressed in the stack semantics gives a new topos-theoretic axiom schema with the full strength of ZF. We call a topos satisfying this schema autological.
We prove two general factorization theorems for fixed-point invariants of fibrations: one for the Lefschetz number and one for the Reidemeister trace.These theorems imply the familiar multiplicativity results for the …
We prove two general factorization theorems for fixed-point invariants of fibrations: one for the Lefschetz number and one for the Reidemeister trace.These theorems imply the familiar multiplicativity results for the Lefschetz and Nielsen numbers of a fibration.Moreover, the proofs of these theorems are essentially formal, taking place in the abstract context of bicategorical traces.This makes generalizations to other contexts straightforward.
We construct a new model category presenting the homotopy theory of presheaves on "inverse EI (∞, 1)-categories", which contains universe objects that satisfy Voevodsky's univalence axiom.In addition to diagrams on …
We construct a new model category presenting the homotopy theory of presheaves on "inverse EI (∞, 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.
The ordinary Structure Identity Principle states that any property of set-level structures (e.g., posets, groups, rings, fields) definable in Univalent Foundations is invariant under isomorphism: more specifically, identifications of structures …
The ordinary Structure Identity Principle states that any property of set-level structures (e.g., posets, groups, rings, fields) definable in Univalent Foundations is invariant under isomorphism: more specifically, identifications of structures coincide with isomorphisms. We prove a version of this principle for a wide range of higher-categorical structures, adapting FOLDS-signatures to specify a general class of structures, and using two-level type theory to treat all categorical dimensions uniformly. As in the previously known case of 1-categories (which is an instance of our theory), the structures themselves must satisfy a local univalence principle, stating that identifications coincide with "isomorphisms" between elements of the structure. Our main technical achievement is a definition of such isomorphisms, which we call "indiscernibilities," using only the dependency structure rather than any notion of composition.
The purpose of this expository note is to describe duality and trace in a symmetric monoidal category, along with important properties (including naturality and functoriality), and to give as many …
The purpose of this expository note is to describe duality and trace in a symmetric monoidal category, along with important properties (including naturality and functoriality), and to give as many examples as possible. Among other things, this note is intended as background for the generalizations to the context of bicategories and indexed monoidal categories.
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.
Cheng, Gurski, and Riehl constructed a cyclic double multicategory of multivariable adjunctions. We show that the same information is carried by a double polycategory, in which opposite categories are polycategorical …
Cheng, Gurski, and Riehl constructed a cyclic double multicategory of multivariable adjunctions. We show that the same information is carried by a double polycategory, in which opposite categories are polycategorical duals. Moreover, this double polycategory is a full substructure of a double Chu construction, whose objects are a sort of polarized category, and which is a natural home for 2-categorical dualities. We obtain the double Chu construction using a general "Chu-Dialectica" construction on polycategories, which includes both the Chu construction and the categorical Dialectica construction of de Paiva. The Chu and Dialectica constructions each impose additional hypotheses making the resulting polycategory representable (hence *-autonomous), but for different reasons; this leads to their apparent differences.
We prove the conjecture that any Grothendieck $(\infty,1)$-topos can be presented by a Quillen model category that interprets homotopy type theory with strict univalent universes. Thus, homotopy type theory can …
We prove the conjecture that any Grothendieck $(\infty,1)$-topos can be presented by a Quillen model category that interprets homotopy type theory with strict univalent universes. Thus, homotopy type theory can be used as a formal language for reasoning internally to $(\infty,1)$-toposes, just as higher-order logic is used for 1-toposes. As part of the proof, we give a new, more explicit, characterization of the fibrations in injective model structures on presheaf categories. In particular, we show that they generalize the coflexible algebras of 2-monad theory.
We show that Voevodsky's univalence axiom for intensional type theory is valid in categories of simplicial presheaves on elegant Reedy categories. In addition to diagrams on inverse categories, as considered …
We show that Voevodsky's univalence axiom for intensional type theory is valid in categories of simplicial presheaves on elegant Reedy categories. In addition to diagrams on inverse categories, as considered in previous work of the author, this includes bisimplicial sets and $\Theta_n$-spaces. This has potential applications to the study of homotopical models for higher categories.
We combine Homotopy Type Theory with axiomatic cohesion, expressing the latter internally with a version of adjoint logic in which the discretization and codiscretization modalities are characterized using a judgmental …
We combine Homotopy Type Theory with axiomatic cohesion, expressing the latter internally with a version of adjoint logic in which the discretization and codiscretization modalities are characterized using a judgmental formalism of crisp variables. This yields type theories that we call spatial and cohesive, in which the types can be viewed as having independent topological and homotopical structure. These type theories can then be used to study formally the process by which topology gives rise to homotopy theory (the fundamental $\infty$-groupoid or shape), disentangling the identifications of Homotopy Type Theory from the paths of topology. In a further refinement called real-cohesion, the shape is determined by continuous maps from the real numbers, as in classical algebraic topology. This enables us to reproduce formally some of the classical applications of homotopy theory to topology. As an example, we prove Brouwer's fixed-point theorem.
The Univalence Principle is the statement that equivalent mathematical structures are indistinguishable. We prove a general version of this principle that applies to all set-based, categorical, and higher-categorical structures defined …
The Univalence Principle is the statement that equivalent mathematical structures are indistinguishable. We prove a general version of this principle that applies to all set-based, categorical, and higher-categorical structures defined in a non-algebraic and space-based style, as well as models of higher-order theories such as topological spaces. In particular, we formulate a general definition of indiscernibility for objects of any such structure, and a corresponding univalence condition that generalizes Rezk’s completeness condition for Segal spaces and ensures that all equivalences of structures are levelwise equivalences. Our work builds on Makkai’s First-Order Logic with Dependent Sorts, but is expressed in Voevodsky’s Univalent Foundations (UF), extending previous work on the Structure Identity Principle and univalent categories in UF. This enables indistinguishability to be expressed simply as identification, and yields a formal theory that is interpretable in classical homotopy theory, but also in other higher topos models. It follows that Univalent Foundations is a fully equivalence-invariant foundation for higher-categorical mathematics, as intended by Voevodsky.
Parametricity is a property of the syntax of type theory implying, e.g., that there is only one function having the type of the polymorphic identity function. Parametricity is usually proven …
Parametricity is a property of the syntax of type theory implying, e.g., that there is only one function having the type of the polymorphic identity function. Parametricity is usually proven externally, and does not hold internally. Internalising it is difficult because once there is a term witnessing parametricity, it also has to be parametric itself and this results in the appearance of higher dimensional cubes. In previous theories with internal parametricity, either an explicit syntax for higher cubes is present or the theory is extended with a new sort for the interval. In this paper we present a type theory with internal parametricity which is a simple extension of Martin-L\"of type theory: there are a few new type formers, term formers and equations. Geometry is not explicit in this syntax, but emergent: the new operations and equations only refer to objects up to dimension 3. We show that this theory is modelled by presheaves over the BCH cube category. Fibrancy conditions are not needed because we use span-based rather than relational parametricity. We define a gluing model for this theory implying that external parametricity and canonicity hold. The theory can be seen as a special case of a new kind of modal type theory, and it is the simplest setting in which the computational properties of higher observational type theory can be demonstrated.
We show that contrary to appearances, Multimodal Type Theory (MTT) over a 2-category M can be interpreted in any M-shaped diagram of categories having, and functors preserving, M-sized limits, without …
We show that contrary to appearances, Multimodal Type Theory (MTT) over a 2-category M can be interpreted in any M-shaped diagram of categories having, and functors preserving, M-sized limits, without the need for extra left adjoints. This is achieved by a construction called "co-dextrification" that co-freely adds left adjoints to any such diagram, which can then be used to interpret the "context lock" functors of MTT. Furthermore, if any of the functors in the diagram have right adjoints, these can also be internalized in type theory as negative modalities in the style of FitchTT. We introduce the name Multimodal Adjoint Type Theory (MATT) for the resulting combined general modal type theory. In particular, we can interpret MATT in any finite diagram of toposes and geometric morphisms, with positive modalities for inverse image functors and negative modalities for direct image functors.
We define and study LNL polycategories, which abstract the judgmental structure of classical linear logic with exponentials. Many existing structures can be represented as LNL polycategories, including LNL adjunctions, linear …
We define and study LNL polycategories, which abstract the judgmental structure of classical linear logic with exponentials. Many existing structures can be represented as LNL polycategories, including LNL adjunctions, linear exponential comonads, LNL multicategories, IL-indexed categories, linearly distributive categories with storage, commutative and strong monads, CBPV-structures, models of polarized calculi, Freyd-categories, and skew multicategories, as well as ordinary cartesian, symmetric, and planar multicategories and monoidal categories, symmetric polycategories, and linearly distributive and *-autonomous categories. To study such classes of structures uniformly, we define a notion of LNL doctrine, such that each of these classes of structures can be identified with the algebras for some such doctrine. We show that free algebras for LNL doctrines can be presented by a sequent calculus, and that every morphism of doctrines induces an adjunction between their 2-categories of algebras.
We show that contrary to appearances, Multimodal Type Theory (MTT) over a 2-category M can be interpreted in any M-shaped diagram of categories having, and functors preserving, M-sized limits, without …
We show that contrary to appearances, Multimodal Type Theory (MTT) over a 2-category M can be interpreted in any M-shaped diagram of categories having, and functors preserving, M-sized limits, without the need for extra left adjoints. This is achieved by a construction called "co-dextrification" that co-freely adds left adjoints to any such diagram, which can then be used to interpret the "context lock" functors of MTT. Furthermore, if any of the functors in the diagram have right adjoints, these can also be internalized in type theory as negative modalities in the style of FitchTT. We introduce the name Multimodal Adjoint Type Theory (MATT) for the resulting combined general modal type theory. In particular, we can interpret MATT in any finite diagram of toposes and geometric morphisms, with positive modalities for inverse image functors and negative modalities for direct image functors.
We introduce Displayed Type Theory (dTT), a multi-modal homotopy type theory with discrete and simplicial modes. In the intended semantics, the discrete mode is interpreted by a model for an …
We introduce Displayed Type Theory (dTT), a multi-modal homotopy type theory with discrete and simplicial modes. In the intended semantics, the discrete mode is interpreted by a model for an arbitrary $\infty$-topos, while the simplicial mode is interpreted by Reedy fibrant augmented semi-simplicial diagrams in that model. This simplicial structure is represented inside the theory by a primitive notion of display or dependency, guarded by modalities, yielding a partially-internal form of unary parametricity. Using the display primitive, we then give a coinductive definition, at the simplicial mode, of a type $\mathsf{SST}$ of semi-simplicial types. Roughly speaking, a semi-simplicial type $X$ consists of a type $X_0$ together with, for each $x:X_0$, a displayed semi-simplicial type over $X$. This mimics how simplices can be generated geometrically through repeated cones, and is made possible by the display primitive at the simplicial mode. The discrete part of $\mathsf{SST}$ then yields the usual infinite indexed definition of semi-simplicial types, both semantically and syntactically. Thus, dTT enables working with semi-simplicial types in full semantic generality.
Abstract We show that numerous distinctive concepts of constructive mathematics arise automatically from an “antithesis” translation of affine logic into intuitionistic logic via a Chu/Dialectica construction. This includes apartness relations, …
Abstract We show that numerous distinctive concepts of constructive mathematics arise automatically from an “antithesis” translation of affine logic into intuitionistic logic via a Chu/Dialectica construction. This includes apartness relations, complemented subsets, anti-subgroups and anti-ideals, strict and non-strict order pairs, cut-valued metrics, and apartness spaces. We also explain the constructive bifurcation of some classical concepts using the choice between multiplicative and additive affine connectives. Affine logic and the antithesis construction thus systematically “constructivize” classical definitions, handling the resulting bookkeeping automatically.
Hofmann and Streicher famously showed how to lift Grothendieck universes into presheaf topoi, and Streicher has extended their result to the case of sheaf topoi by sheafification. In parallel, van …
Hofmann and Streicher famously showed how to lift Grothendieck universes into presheaf topoi, and Streicher has extended their result to the case of sheaf topoi by sheafification. In parallel, van den Berg and Moerdijk have shown in the context of algebraic set theory that similar constructions continue to apply even in weaker metatheories. Unfortunately, sheafification seems not to preserve an important realignment property enjoyed by the presheaf universes that plays a critical role in models of univalent type theory as well as synthetic Tait computability, a recent technique to establish syntactic properties of type theories and programming languages. In the context of multiple universes, the realignment property also implies a coherent choice of codes for connectives at each universe level, thereby interpreting the cumulativity laws present in popular formulations of Martin-L\"of type theory. We observe that a slight adjustment to an argument of Shulman constructs a cumulative universe hierarchy satisfying the realignment property at every level in any Grothendieck topos. Hence one has direct-style interpretations of Martin-L\"of type theory with cumulative universes into all Grothendieck topoi. A further implication is to extend the reach of recent synthetic methods in the semantics of cubical type theory and the syntactic metatheory of type theory and programming languages to all Grothendieck topoi.
Based on Taylor's hereditarily directed plump ordinals, we define the directed plump ordering on W-types in Martin-L\"of type theory. This ordering is similar to the plump ordering but comes equipped …
Based on Taylor's hereditarily directed plump ordinals, we define the directed plump ordering on W-types in Martin-L\"of type theory. This ordering is similar to the plump ordering but comes equipped with non-empty finite joins in addition to the usual properties of the plump ordering.
We prove 2-categorical conservativity for any {0,T}-free fragment of MALL over its corresponding intuitionistic version: that is, that the universal map from a closed symmetric monoidal category to the *-autonomous …
We prove 2-categorical conservativity for any {0,T}-free fragment of MALL over its corresponding intuitionistic version: that is, that the universal map from a closed symmetric monoidal category to the *-autonomous category that it freely generates is fully faithful, and similarly for other doctrines. This implies that linear logics and graphical calculi for *-autonomous categories can also be interpreted canonically in closed symmetric monoidal categories. In particular, every closed symmetric monoidal category can be fully embedded in a *-autonomous category, preserving both tensor products and internal-homs. In fact, we prove this directly first with a Yoneda-style embedding (an enhanced "Hyland envelope" that can be regarded as a polycategorical form of Day convolution), and deduce 2-conservativity afterwards from Hyland-Schalk double gluing and a technique of Lafont. The same is true for other fragments of *-autonomous structure, such as linear distributivity, and the embedding can be enhanced to preserve any desired family of nonempty limits and colimits.
Magnitude is a numerical invariant of enriched categories, including in particular metric spaces as [0, ∞)-enriched categories.We show that in many cases magnitude can be categorified to a homology theory …
Magnitude is a numerical invariant of enriched categories, including in particular metric spaces as [0, ∞)-enriched categories.We show that in many cases magnitude can be categorified to a homology theory for enriched categories, which we call magnitude homology (in fact, it is a special sort of Hochschild homology), whose graded Euler characteristic is the magnitude.Magnitude homology of metric spaces generalizes the Hepworth-Willerton magnitude homology of graphs, and detects geometric information such as convexity.
We give a natural-deduction-style type theory for symmetric monoidal categories whose judgmental structure directly represents morphisms with tensor products in their codomain as well as their domain. The syntax is …
We give a natural-deduction-style type theory for symmetric monoidal categories whose judgmental structure directly represents morphisms with tensor products in their codomain as well as their domain. The syntax is inspired by Sweedler notation for coalgebras, with variables associated to types in the domain and terms associated to types in the codomain, allowing types to be treated informally like sets with elements subject to global linearity-like restrictions. We illustrate the usefulness of this type theory with various applications to duality, traces, Frobenius monoids, and (weak) Hopf monoids.
We show that a derivator is stable if and only if homotopy finite limits and homotopy finite colimits commute, if and only if homotopy finite limit functors have right adjoints, …
We show that a derivator is stable if and only if homotopy finite limits and homotopy finite colimits commute, if and only if homotopy finite limit functors have right adjoints, and if and only if homotopy finite colimit functors have left adjoints. These characterizations generalize to an abstract notion of "stability relative to a class of functors", which includes in particular pointedness, semiadditivity, and ordinary stability. To prove them, we develop the theory of derivators enriched over monoidal left derivators and weighted homotopy limits and colimits therein.
Without the axiom of choice, the free exact completion of the category of sets (i.e. the category of setoids) may not be complete or cocomplete. We will show that nevertheless, …
Without the axiom of choice, the free exact completion of the category of sets (i.e. the category of setoids) may not be complete or cocomplete. We will show that nevertheless, it can be enhanced to a derivator: the formal structure of categories of diagrams related by Kan extension functors. Moreover, this derivator is the free cocompletion of a point in a class of 1-truncated (which behave like a 1-category rather than a higher category).
In classical mathematics, the free cocompletion of a point relative to all derivators is the homotopy theory of spaces. Thus, if there is a homotopy theory that can be shown to have this universal property constructively, its 1-truncation must contain not only sets, but also setoids. This suggests that either setoids are an unavoidable aspect of constructive homotopy theory, or more radical modifications to the notion of homotopy theory are needed.
This is an introduction to type theory, synthetic topology, and homotopy type theory from a category-theoretic and topological point of view, written as a chapter for the book New Spaces …
This is an introduction to type theory, synthetic topology, and homotopy type theory from a category-theoretic and topological point of view, written as a chapter for the book New Spaces for Mathematics and Physics (ed. Gabriel Catren and Mathieu Anel).
The Univalence Principle is the statement that equivalent mathematical structures are indistinguishable. We prove a general version of this principle that applies to all set-based, categorical, and higher-categorical structures defined …
The Univalence Principle is the statement that equivalent mathematical structures are indistinguishable. We prove a general version of this principle that applies to all set-based, categorical, and higher-categorical structures defined in a non-algebraic and space-based style, as well as models of higher-order theories such as topological spaces. In particular, we formulate a general definition of indiscernibility for objects of any such structure, and a corresponding univalence condition that generalizes Rezk's completeness condition for Segal spaces and ensures that all equivalences of structures are levelwise equivalences.
Our work builds on Makkai's First-Order Logic with Dependent Sorts, but is expressed in Voevodsky's Univalent Foundations (UF), extending previous work on the Structure Identity Principle and univalent categories in UF. This enables indistinguishability to be expressed simply as identification, and yields a formal theory that is interpretable in classical homotopy theory, but also in other higher topos models. It follows that Univalent Foundations is a fully equivalence-invariant foundation for higher-categorical mathematics, as intended by Voevodsky.
We show that the type TZ of Z-torsors has the dependent universal property of the circle, which characterizes it up to a unique homotopy equivalence. The construction uses Voevodsky's Univalence …
We show that the type TZ of Z-torsors has the dependent universal property of the circle, which characterizes it up to a unique homotopy equivalence. The construction uses Voevodsky's Univalence Axiom and propositional truncation, yielding a stand-alone construction of the circle not using higher inductive types.
We present a unified framework for Petri nets and various variants, such as pre-nets and Kock's whole-grain Petri nets. Our framework is based on a less well-studied notion that we …
We present a unified framework for Petri nets and various variants, such as pre-nets and Kock's whole-grain Petri nets. Our framework is based on a less well-studied notion that we call $\Sigma$-nets, which allow finer control over whether tokens are treated using the collective or individual token philosophy. We describe three forms of execution semantics in which pre-nets generate strict monoidal categories, $\Sigma$-nets (including whole-grain Petri nets) generate symmetric strict monoidal categories, and Petri nets generate commutative monoidal categories, all by left adjoint functors. We also construct adjunctions relating these categories of nets to each other, in particular showing that all kinds of net can be embedded in the unifying category of $\Sigma$-nets, in a way that commutes coherently with their execution semantics.
We define and study LNL polycategories, which abstract the judgmental structure of classical linear logic with exponentials. Many existing structures can be represented as LNL polycategories, including LNL adjunctions, linear …
We define and study LNL polycategories, which abstract the judgmental structure of classical linear logic with exponentials. Many existing structures can be represented as LNL polycategories, including LNL adjunctions, linear exponential comonads, LNL multicategories, IL-indexed categories, linearly distributive categories with storage, commutative and strong monads, CBPV-structures, models of polarized calculi, Freyd-categories, and skew multicategories, as well as ordinary cartesian, symmetric, and planar multicategories and monoidal categories, symmetric polycategories, and linearly distributive and *-autonomous categories. To study such classes of structures uniformly, we define a notion of LNL doctrine, such that each of these classes of structures can be identified with the algebras for some such doctrine. We show that free algebras for LNL doctrines can be presented by a sequent calculus, and that every morphism of doctrines induces an adjunction between their 2-categories of algebras.
The Univalence Principle is the statement that equivalent mathematical structures are indistinguishable. We prove a general version of this principle that applies to all set-based, categorical, and higher-categorical structures defined …
The Univalence Principle is the statement that equivalent mathematical structures are indistinguishable. We prove a general version of this principle that applies to all set-based, categorical, and higher-categorical structures defined in a non-algebraic and space-based style, as well as models of higher-order theories such as topological spaces. In particular, we formulate a general definition of indiscernibility for objects of any such structure, and a corresponding univalence condition that generalizes Rezk's completeness condition for Segal spaces and ensures that all equivalences of structures are levelwise equivalences. Our work builds on Makkai's First-Order Logic with Dependent Sorts, but is expressed in Voevodsky's Univalent Foundations (UF), extending previous work on the Structure Identity Principle and univalent categories in UF. This enables indistinguishability to be expressed simply as identification, and yields a formal theory that is interpretable in classical homotopy theory, but also in other higher topos models. It follows that Univalent Foundations is a fully equivalence-invariant foundation for higher-categorical mathematics, as intended by Voevodsky.
We present a unified framework for Petri nets and various variants, such as pre-nets and Kock's whole-grain Petri nets. Our framework is based on a less well-studied notion that we …
We present a unified framework for Petri nets and various variants, such as pre-nets and Kock's whole-grain Petri nets. Our framework is based on a less well-studied notion that we call $Σ$-nets, which allow finer control over whether tokens are treated using the collective or individual token philosophy. We describe three forms of execution semantics in which pre-nets generate strict monoidal categories, $Σ$-nets (including whole-grain Petri nets) generate symmetric strict monoidal categories, and Petri nets generate commutative monoidal categories, all by left adjoint functors. We also construct adjunctions relating these categories of nets to each other, in particular showing that all kinds of net can be embedded in the unifying category of $Σ$-nets, in a way that commutes coherently with their execution semantics.
Without the axiom of choice, the free exact completion of the category of sets (i.e. the category of setoids) may not be complete or cocomplete. We will show that nevertheless, …
Without the axiom of choice, the free exact completion of the category of sets (i.e. the category of setoids) may not be complete or cocomplete. We will show that nevertheless, it can be enhanced to a derivator: the formal structure of categories of diagrams related by Kan extension functors. Moreover, this derivator is the free cocompletion of a point in a class of "1-truncated derivators" (which behave like a 1-category rather than a higher category). In classical mathematics, the free cocompletion of a point relative to all derivators is the homotopy theory of spaces. Thus, if there is a homotopy theory that can be shown to have this universal property constructively, its 1-truncation must contain not only sets, but also setoids. This suggests that either setoids are an unavoidable aspect of constructive homotopy theory, or more radical modifications to the notion of homotopy theory are needed.
The ordinary Structure Identity Principle states that any property of set-level structures (e.g., posets, groups, rings, fields) definable in Univalent Foundations is invariant under isomorphism: more specifically, identifications of structures …
The ordinary Structure Identity Principle states that any property of set-level structures (e.g., posets, groups, rings, fields) definable in Univalent Foundations is invariant under isomorphism: more specifically, identifications of structures coincide with isomorphisms. We prove a version of this principle for a wide range of higher-categorical structures, adapting FOLDS-signatures to specify a general class of structures, and using two-level type theory to treat all categorical dimensions uniformly. As in the previously known case of 1-categories (which is an instance of our theory), the structures themselves must satisfy a local univalence principle, stating that identifications coincide with "isomorphisms" between elements of the structure. Our main technical achievement is a definition of such isomorphisms, which we call "indiscernibilities," using only the dependency structure rather than any notion of composition.
We show the doctrine of $\ast$-autonomous categories is 2-conservative over the doctrine of closed symmetric monoidal categories, i.e. the universal map from a closed symmetric monoidal category to the $\ast$-autonomous …
We show the doctrine of $\ast$-autonomous categories is 2-conservative over the doctrine of closed symmetric monoidal categories, i.e. the universal map from a closed symmetric monoidal category to the $\ast$-autonomous category that it freely generates is fully faithful. This implies that linear logics and graphical calculi for $\ast$-autonomous categories can also be interpreted canonically in closed symmetric monoidal categories. In particular, our result implies that every closed symmetric monoidal category can be fully embedded in a $\ast$-autonomous category, preserving both tensor products and internal-homs. But in fact we prove this directly first with a Yoneda-style embedding (an enhanced Hyland envelope that can be regarded as a polycategorical form of Day convolution), and deduce 2-conservativity afterwards from double gluing and a technique of Lafont. Since our method uses polycategories, it also applies to other fragments of $\ast$-autonomous structure, such as linear distributivity. It can also be enhanced to preserve any desired family of nonempty limits and colimits.
We show the doctrine of $\ast$-autonomous categories is 2-conservative over the doctrine of closed symmetric monoidal categories, i.e. the universal map from a closed symmetric monoidal category to the $\ast$-autonomous …
We show the doctrine of $\ast$-autonomous categories is 2-conservative over the doctrine of closed symmetric monoidal categories, i.e. the universal map from a closed symmetric monoidal category to the $\ast$-autonomous category that it freely generates is fully faithful. This implies that linear logics and graphical calculi for $\ast$-autonomous categories can also be interpreted canonically in closed symmetric monoidal categories. In particular, our result implies that every closed symmetric monoidal category can be fully embedded in a $\ast$-autonomous category, preserving both tensor products and internal-homs. But in fact we prove this directly first with a Yoneda-style embedding (an enhanced Hyland envelope that can be regarded as a polycategorical form of Day convolution), and deduce 2-conservativity afterwards from double gluing and a technique of Lafont. Since our method uses polycategories, it also applies to other fragments of $\ast$-autonomous structure, such as linear distributivity. It can also be enhanced to preserve any desired family of nonempty limits and colimits.
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 show that the type $\mathrm{T}\mathbb{Z}$ of $\mathbb{Z}$-torsors has the dependent universal property of the circle, which characterizes it up to a unique homotopy equivalence. The construction uses Voevodsky's Univalence …
We show that the type $\mathrm{T}\mathbb{Z}$ of $\mathbb{Z}$-torsors has the dependent universal property of the circle, which characterizes it up to a unique homotopy equivalence. The construction uses Voevodsky's Univalence Axiom and propositional truncation, yielding a stand-alone construction of the circle not using higher inductive types.
Higher inductive types are a class of type-forming rules, introduced to provide basic (and not-so-basic) homotopy-theoretic constructions in a type-theoretic style. They have proven very fruitful for the "synthetic" development …
Higher inductive types are a class of type-forming rules, introduced to provide basic (and not-so-basic) homotopy-theoretic constructions in a type-theoretic style. They have proven very fruitful for the "synthetic" development of homotopy theory within type theory, as well as in formalizing ordinary set-level mathematics in type theory. In this article, we construct models of a wide range of higher inductive types in a fairly wide range of settings. We introduce the notion of cell monad with parameters: a semantically-defined scheme for specifying homotopically well-behaved notions of structure. We then show that any suitable model category has *weakly stable typal initial algebras* for any cell monad with parameters. When combined with the local universes construction to obtain strict stability, this specializes to give models of specific higher inductive types, including spheres, the torus, pushout types, truncations, the James construction, and general localisations. Our results apply in any sufficiently nice Quillen model category, including any right proper, simplicially locally cartesian closed, simplicial Cisinski model category (such as simplicial sets) and any locally presentable locally cartesian closed category (such as sets) with its trivial model structure. In particular, any locally presentable locally cartesian closed $(\infty,1)$-category is presented by some model category to which our results apply.
We prove the conjecture that any Grothendieck $(\infty,1)$-topos can be presented by a Quillen model category that interprets homotopy type theory with strict univalent universes. Thus, homotopy type theory can …
We prove the conjecture that any Grothendieck $(\infty,1)$-topos can be presented by a Quillen model category that interprets homotopy type theory with strict univalent universes. Thus, homotopy type theory can be used as a formal language for reasoning internally to $(\infty,1)$-toposes, just as higher-order logic is used for 1-toposes. As part of the proof, we give a new, more explicit, characterization of the fibrations in injective model structures on presheaf categories. In particular, we show that they generalize the coflexible algebras of 2-monad theory.
We present a method of constructing monoidal, braided monoidal, and symmetric monoidal bicategories from corresponding types of monoidal double categories that satisfy a lifting condition. Many important monoidal bicategories arise …
We present a method of constructing monoidal, braided monoidal, and symmetric monoidal bicategories from corresponding types of monoidal double categories that satisfy a lifting condition. Many important monoidal bicategories arise naturally in this way, and applying our general method is much easier than explicitly verifying the coherence laws of a monoidal bicategory for each example. Abstracting from earlier work in this direction, we express the construction as a functor between locally cubical bicategories that preserves monoid objects; this ensures that it also preserves monoidal functors, transformations, adjunctions, and so on. Examples include the monoidal bicategories of algebras and bimodules, categories and profunctors, sets and spans, open Markov processes, parametrized spectra, and various functors relating them.
We give a natural-deduction-style type theory for symmetric monoidal categories whose judgmental structure directly represents morphisms with tensor products in their codomain as well as their domain. The syntax is …
We give a natural-deduction-style type theory for symmetric monoidal categories whose judgmental structure directly represents morphisms with tensor products in their codomain as well as their domain. The syntax is inspired by Sweedler notation for coalgebras, with variables associated to types in the domain and terms associated to types in the codomain, allowing types to be treated informally like "sets with elements" subject to global linearity-like restrictions. We illustrate the usefulness of this type theory with various applications to duality, traces, Frobenius monoids, and (weak) Hopf monoids.
We show that the type $\mathrm{T}\mathbb{Z}$ of $\mathbb{Z}$-torsors has the dependent universal property of the circle, which characterizes it up to a unique homotopy equivalence. The construction uses Voevodsky's Univalence …
We show that the type $\mathrm{T}\mathbb{Z}$ of $\mathbb{Z}$-torsors has the dependent universal property of the circle, which characterizes it up to a unique homotopy equivalence. The construction uses Voevodsky's Univalence Axiom and propositional truncation, yielding a stand-alone construction of the circle not using higher inductive types.
We prove the conjecture that any Grothendieck $(\infty,1)$-topos can be presented by a Quillen model category that interprets homotopy type theory with strict univalent universes. Thus, homotopy type theory can …
We prove the conjecture that any Grothendieck $(\infty,1)$-topos can be presented by a Quillen model category that interprets homotopy type theory with strict univalent universes. Thus, homotopy type theory can be used as a formal language for reasoning internally to $(\infty,1)$-toposes, just as higher-order logic is used for 1-toposes. As part of the proof, we give a new, more explicit, characterization of the fibrations in injective model structures on presheaf categories. In particular, we show that they generalize the coflexible algebras of 2-monad theory.
We show that numerous distinctive concepts of constructive mathematics arise automatically from an interpretation of higher-order into intuitionistic higher-order logic via a Chu construction. This includes apartness relations, complemented subsets, …
We show that numerous distinctive concepts of constructive mathematics arise automatically from an interpretation of higher-order into intuitionistic higher-order logic via a Chu construction. This includes apartness relations, complemented subsets, anti-subgroups and anti-ideals, strict and non-strict order pairs, cut-valued metrics, and apartness spaces. We also explain the constructive bifurcation of classical concepts using the choice between multiplicative and additive linear connectives. Linear logic thus systematically constructivizes classical definitions and deals automatically with the resulting bookkeeping, and could potentially be used directly as a basis for constructive mathematics in place of intuitionistic logic.
Homotopy type theory and univalent foundations (HoTT/UF) is a new foundation of mathematics, based not on set theory but on “infinity-groupoids”, which consist of collections of objects, ways in which …
Homotopy type theory and univalent foundations (HoTT/UF) is a new foundation of mathematics, based not on set theory but on “infinity-groupoids”, which consist of collections of objects, ways in which two objects can be equal, ways in which those ways-to-be-equal can be equal, ad infinitum. Though apparently complicated, such structures are increasingly important in mathematics. Philosophically, they are an inevitable result of the notion that whenever we form a collection of things, we must simultaneously consider when two of those things are the same. The “synthetic” nature of HoTT/UF enables a much simpler description of infinity groupoids than is available in set theory, thereby aligning with modern mathematics while placing “equality” back in the foundations of logic. This chapter will introduce the basic ideas of HoTT/UF for a philosophical audience, including Voevodsky’s univalence axiom and higher inductive types.
Cheng, Gurski, and Riehl constructed a cyclic double multicategory of multivariable adjunctions. We show that the same information is carried by a double polycategory, in which opposite categories are polycategorical …
Cheng, Gurski, and Riehl constructed a cyclic double multicategory of multivariable adjunctions. We show that the same information is carried by a double polycategory, in which opposite categories are polycategorical duals. Moreover, this double polycategory is a full substructure of a double Chu construction, whose objects are a sort of polarized category, and which is a natural home for 2-categorical dualities. We obtain the double Chu construction using a general "Chu-Dialectica" construction on polycategories, which includes both the Chu construction and the categorical Dialectica construction of de Paiva. The Chu and Dialectica constructions each impose additional hypotheses making the resulting polycategory representable (hence *-autonomous), but for different reasons; this leads to their apparent differences.
We prove two general decomposition theorems for fixed-point invariants: one for the Lefschetz number and one for the Reidemeister trace.These theorems imply the familiar additivity results for these invariants.Moreover, the …
We prove two general decomposition theorems for fixed-point invariants: one for the Lefschetz number and one for the Reidemeister trace.These theorems imply the familiar additivity results for these invariants.Moreover, the proofs of these theorems are essentially formal, taking place in the abstract context of bicategorical traces.This makes it straightforward to generalize the theory to analogous invariants in other contexts, such as equivariant and fiberwise homotopy theory.
Magnitude is a numerical invariant of enriched categories, including in particular metric spaces as $[0,\infty)$-enriched categories. We show that in many cases magnitude can be categorified to a homology theory …
Magnitude is a numerical invariant of enriched categories, including in particular metric spaces as $[0,\infty)$-enriched categories. We show that in many cases magnitude can be categorified to a homology theory for enriched categories, which we call magnitude homology (in fact, it is a special sort of Hochschild homology), whose graded Euler characteristic is the magnitude. Magnitude homology of metric spaces generalizes the Hepworth--Willerton magnitude homology of graphs, and detects geometric information such as convexity.
We combine homotopy type theory with axiomatic cohesion, expressing the latter internally with a version of ‘adjoint logic’ in which the discretization and codiscretization modalities are characterized using a judgemental …
We combine homotopy type theory with axiomatic cohesion, expressing the latter internally with a version of ‘adjoint logic’ in which the discretization and codiscretization modalities are characterized using a judgemental formalism of ‘crisp variables.’ This yields type theories that we call ‘spatial’ and ‘cohesive,’ in which the types can be viewed as having independent topological and homotopical structure. These type theories can then be used to study formally the process by which topology gives rise to homotopy theory (the ‘fundamental ∞-groupoid’ or ‘shape’), disentangling the ‘identifications’ of homotopy type theory from the ‘continuous paths’ of topology. In a further refinement called ‘real-cohesion,’ the shape is determined by continuous maps from the real numbers, as in classical algebraic topology. This enables us to reproduce formally some of the classical applications of homotopy theory to topology. As an example, we prove Brouwer's fixed-point theorem.
It is known that one can construct non-parametric functions by assuming classical axioms. Our work is a converse to that: we prove classical axioms in dependent type theory assuming specific …
It is known that one can construct non-parametric functions by assuming classical axioms. Our work is a converse to that: we prove classical axioms in dependent type theory assuming specific instan ...
We propose foundations for a synthetic theory of $(\infty,1)$-categories within homotopy type theory. We axiomatize a directed interval type, then define higher simplices from it and use them to probe …
We propose foundations for a synthetic theory of $(\infty,1)$-categories within homotopy type theory. We axiomatize a directed interval type, then define higher simplices from it and use them to probe the internal categorical structures of arbitrary types. We define Segal types, in which binary composites exist uniquely up to homotopy; this automatically ensures composition is coherently associative and unital at all dimensions. We define Rezk types, in which the categorical isomorphisms are additionally equivalent to the type-theoretic identities - a local univalence condition. And we define covariant fibrations, which are type families varying functorially over a Segal type, and prove a dependent Yoneda lemma that can be viewed as a directed form of the usual elimination rule for identity types. We conclude by studying homotopically correct adjunctions between Segal types, and showing that for a functor between Rezk to have an adjoint is a mere proposition.
To make the bookkeeping in such proofs manageable, we use a three-layered type theory with shapes, whose contexts are extended by polytopes within directed cubes, which can be abstracted over using extension types that generalize the path-types of cubical type theory. In an appendix, we describe the motivating semantics in the Reedy model structure on bisimplicial sets, in which our Segal and Rezk correspond to Segal spaces and complete Segal spaces.
We study idempotents in intensional Martin-L\"of type theory, and in particular the question of when and whether they split. We show that in the presence of propositional truncation and Voevodsky's …
We study idempotents in intensional Martin-L\"of type theory, and in particular the question of when and whether they split. We show that in the presence of propositional truncation and Voevodsky's univalence axiom, there exist idempotents that do not split; thus in plain MLTT not all idempotents can be proven to split. On the other hand, assuming only function extensionality, an idempotent can be split if and only if its witness of idempotency satisfies one extra coherence condition. Both proofs are inspired by parallel results of Lurie in higher category theory, showing that ideas from higher category theory and homotopy theory can have applications even in ordinary MLTT. Finally, we show that although the witness of idempotency can be recovered from a splitting, the one extra coherence condition cannot in general; and we construct "the type of fully coherent idempotents", by splitting an idempotent on the type of partially coherent ones. Our results have been formally verified in the proof assistant Coq.
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.
It is known that one can construct non-parametric functions by assuming classical axioms. Our work is a converse to that: we prove classical axioms in dependent type theory assuming specific …
It is known that one can construct non-parametric functions by assuming classical axioms. Our work is a converse to that: we prove classical axioms in dependent type theory assuming specific instances of non-parametricity. We also address the interaction between classical axioms and the existence of automorphisms of a type universe. We work over intensional Martin-Löf dependent type theory, and in some results assume further principles including function extensionality, propositional extensionality, propositional truncation, and the univalence axiom.
We construct a new model category presenting the homotopy theory of presheaves on "inverse EI (∞, 1)-categories", which contains universe objects that satisfy Voevodsky's univalence axiom.In addition to diagrams on …
We construct a new model category presenting the homotopy theory of presheaves on "inverse EI (∞, 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.
This is an introduction to type theory, synthetic topology, and homotopy type theory from a category-theoretic and topological point of view, written as a chapter for the book "New Spaces …
This is an introduction to type theory, synthetic topology, and homotopy type theory from a category-theoretic and topological point of view, written as a chapter for the book "New Spaces for Mathematics and Physics" (ed. Gabriel Catren and Mathieu Anel).
We propose foundations for a synthetic theory of $(\infty,1)$-categories within homotopy type theory. We axiomatize a directed interval type, then define higher simplices from it and use them to probe …
We propose foundations for a synthetic theory of $(\infty,1)$-categories within homotopy type theory. We axiomatize a directed interval type, then define higher simplices from it and use them to probe the internal categorical structures of arbitrary types. We define Segal types, in which binary composites exist uniquely up to homotopy; this automatically ensures composition is coherently associative and unital at all dimensions. We define Rezk types, in which the categorical isomorphisms are additionally equivalent to the type-theoretic identities - a "local univalence" condition. And we define covariant fibrations, which are type families varying functorially over a Segal type, and prove a "dependent Yoneda lemma" that can be viewed as a directed form of the usual elimination rule for identity types. We conclude by studying homotopically correct adjunctions between Segal types, and showing that for a functor between Rezk types to have an adjoint is a mere proposition. To make the bookkeeping in such proofs manageable, we use a three-layered type theory with shapes, whose contexts are extended by polytopes within directed cubes, which can be abstracted over using "extension types" that generalize the path-types of cubical type theory. In an appendix, we describe the motivating semantics in the Reedy model structure on bisimplicial sets, in which our Segal and Rezk types correspond to Segal spaces and complete Segal spaces.
We report on the development of the HoTT library, a formalization of homotopy type theory in the Coq proof assistant. It formalizes most of basic homotopy type theory, including univalence, …
We report on the development of the HoTT library, a formalization of homotopy type theory in the Coq proof assistant. It formalizes most of basic homotopy type theory, including univalence, higher inductive types, and significant amounts of synthetic homotopy theory, as well as category theory and modalities. The library has been used as a basis for several independent developments. We discuss the decisions that led to the design of the library, and we comment on the interaction of homotopy type theory with recently introduced features of Coq, such as universe polymorphism and private inductive types.
Homotopy type theory is a recent research area connecting type theory with homotopy theory by interpreting types as spaces. In particular, one can prove and mechanize type-theoretic analogues of homotopy-theoretic …
Homotopy type theory is a recent research area connecting type theory with homotopy theory by interpreting types as spaces. In particular, one can prove and mechanize type-theoretic analogues of homotopy-theoretic theorems, yielding homotopy theory. Here we consider the Seifert-van Kampen theorem, which characterizes the loop structure of spaces obtained by gluing. This is useful in homotopy theory because many spaces are constructed by gluing, and the loop structure helps distinguish distinct spaces. The synthetic proof showcases many new characteristics of synthetic homotopy theory, such as the encode-decode method, enforced homotopy-invariance, and lack of underlying sets.
In some bicategories, the 1-cells are `morphisms' between the 0-cells, such as functors between categories, but in others they are `objects' over the 0-cells, such as bimodules, spans, distributors, or …
In some bicategories, the 1-cells are `morphisms' between the 0-cells, such as functors between categories, but in others they are `objects' over the 0-cells, such as bimodules, spans, distributors, or parametrized spectra. Many bicategorical notions do not work well in these cases, because the `morphisms between 0-cells', such as ring homomorphisms, are missing. We can include them by using a pseudo double category, but usually these morphisms also induce base change functors acting on the 1-cells. We avoid complicated coherence problems by describing base change `nonalgebraically', using categorical fibrations. The resulting `framed bicategories' assemble into 2-categories, with attendant notions of equivalence, adjunction, and so on which are more appropriate for our examples than are the usual bicategorical ones.
We then describe two ways to construct framed bicategories. One is an analogue of rings and bimodules which starts from one framed bicategory and builds another. The other starts from a `monoidal fibration', meaning a parametrized family of monoidal categories, and produces an analogue of the framed bicategory of spans. Combining the two, we obtain a construction which includes both enriched and internal categories as special cases.
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.
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.
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.
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.
Prologue Point-set topology, change functors, and proper actions: Introduction to Part I The point-set topology of parametrized spaces Change functors and compatibility relations Proper actions, equivariant bundles and fibrations Model …
Prologue Point-set topology, change functors, and proper actions: Introduction to Part I The point-set topology of parametrized spaces Change functors and compatibility relations Proper actions, equivariant bundles and fibrations Model categories and parametrized spaces: Introduction to Part II Topologically bicomplete model categories Well-grounded topological model categories The $qf$-model structure on $\mathcal{K}_B$ Equivariant $qf$-type model structures Ex-fibrations and ex-quasifibrations The equivalence between Ho$G\mathcal{K}_B$ and $hG\mathcal{W}_B$ Parametrized equivariant stable homotopy theory: Introduction to Part III Enriched categories and $G$-categories The category of orthogonal $G$-spectra over $B$ Model structures for parametrized $G$-spectra Adjunctions and compatibility relations Module categories, change of universe, and change of groups Parametrized duality theory: Introduction to Part IV Fiberwise duality and transfer maps Closed symmetric bicategories The closed symmetric bicategory of parametrized spectra Costenoble-Waner duality Fiberwise Costenoble-Waner duality Homology and cohomology, Thom spectra, and addenda: Introduction to Part V Parametrized homology and cohomology theories Equivariant parametrized homology and cohomology Twisted theories and spectral sequences Parametrized FSP's and generalized Thom spectra Epilogue: Cellular philosophy and alternative approaches Bibliography Index Index of notation.
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 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.
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.
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.
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].
By the Lefschetz fixed point theorem, if an endomorphism of a topological space is fixed-point-free, then its Lefschetz number vanishes. This necessary condition is not usually sufficient, however; for that …
By the Lefschetz fixed point theorem, if an endomorphism of a topological space is fixed-point-free, then its Lefschetz number vanishes. This necessary condition is not usually sufficient, however; for that we need a refinement of the Lefschetz number called the Reidemeister trace. Abstractly, the Lefschetz number is a trace in a symmetric monoidal category, while the Reidemeister trace is a trace in a bicategory; in this paper we relate these contexts using indexed symmetric monoidal categories. In particular, we will show that for any symmetric monoidal category with an associated indexed symmetric monoidal category, there is an associated bicategory which produces refinements of trace analogous to the Reidemeister trace. This bicategory also produces a new notion of trace for parametrized spaces with dualizable fibers, which refines the obvious "fiberwise" traces by incorporating the action of the fundamental group of the base space. We also advance the basic theory of indexed monoidal categories, including introducing a string diagram calculus which makes calculations much more tractable. This abstract framework lays the foundation for generalizations of these ideas to other contexts.
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-Löf type theory with one univalent universe (formulated in terms of contextual categories) is at least as consistent as ZFC with two inaccessible cardinals.
We present a new coherence theorem for comprehension categories, providing strict models of dependent type theory with all standard constructors, including dependent products, dependent sums, identity types, and other inductive …
We present a new coherence theorem for comprehension categories, providing strict models of dependent type theory with all standard constructors, including dependent products, dependent sums, identity types, and other inductive types. Precisely, we take as input a “weak model”: a comprehension category, equipped with structure corresponding to the desired logical constructions. We assume throughout that the base category is close to locally Cartesian closed: specifically, that products and certain exponentials exist. Beyond this, we require only that the logical structure should be weakly stable—a pure existence statement, not involving any specific choice of structure, weaker than standard categorical Beck--Chevalley conditions, and holding in the now standard homotopy-theoretic models of type theory. Given such a comprehension category, we construct an equivalent split one whose logical structure is strictly stable under reindexing. This yields an interpretation of type theory with the chosen constructors. The model is adapted from Voevodsky's use of universes for coherence, and at the level of fibrations is a classical construction of Giraud. It may be viewed in terms of local universes or delayed substitutions.
Higher inductive types are a class of type-forming rules, introduced to provide basic (and not-so-basic) homotopy-theoretic constructions in a type-theoretic style. They have proven very fruitful for the "synthetic" development …
Higher inductive types are a class of type-forming rules, introduced to provide basic (and not-so-basic) homotopy-theoretic constructions in a type-theoretic style. They have proven very fruitful for the "synthetic" development of homotopy theory within type theory, as well as in formalizing ordinary set-level mathematics in type theory. In this article, we construct models of a wide range of higher inductive types in a fairly wide range of settings. We introduce the notion of cell monad with parameters: a semantically-defined scheme for specifying homotopically well-behaved notions of structure. We then show that any suitable model category has *weakly stable typal initial algebras* for any cell monad with parameters. When combined with the local universes construction to obtain strict stability, this specializes to give models of specific higher inductive types, including spheres, the torus, pushout types, truncations, the James construction, and general localisations. Our results apply in any sufficiently nice Quillen model category, including any right proper, simplicially locally cartesian closed, simplicial Cisinski model category (such as simplicial sets) and any locally presentable locally cartesian closed category (such as sets) with its trivial model structure. In particular, any locally presentable locally cartesian closed $(\infty,1)$-category is presented by some model category to which our results apply.
We develop some aspects of the theory of derivators, pointed derivators, and stable derivators. As a main result, we show that the values of a stable derivator can be canonically …
We develop some aspects of the theory of derivators, pointed derivators, and stable derivators. As a main result, we show that the values of a stable derivator can be canonically endowed with the structure of a triangulated category. Moreover, the functors belonging to the stable derivator can be turned into exact functors with respect to these triangulated structures. Along the way, we give a simplification of the axioms of a pointed derivator and a reformulation of the base change axiom in terms of Grothendieck (op)fibration. Furthermore, we have a new proof that a combinatorial model category has an underlying derivator.
The Lefschetz fixed point theorem follows easily from the identification of the Lefschetz number with the fixed point index. This identification is a consequence of the functoriality of the trace …
The Lefschetz fixed point theorem follows easily from the identification of the Lefschetz number with the fixed point index. This identification is a consequence of the functoriality of the trace in symmetric monoidal categories. There are refinements of the Lefschetz number and the fixed point index that give a converse to the Lefschetz fixed point theorem. An important part of this theorem is the identification of these different invariants. We define a generalization of the trace in symmetric monoidal categories to a trace in bicategories with shadows. We show the invariants used in the converse of the Lefschetz fixed point theorem are examples of this trace and that the functoriality of the trace provides some of the necessary identifications. The methods used here do not use simplicial techniques and so generalize readily to other contexts.
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.
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 show that Voevodsky's univalence axiom for homotopy type theory is valid in categories of simplicial presheaves on elegant Reedy categories.In addition to diagrams on inverse categories, as considered in …
We show that Voevodsky's univalence axiom for homotopy type theory is valid in categories of simplicial presheaves on elegant Reedy categories.In addition to diagrams on inverse categories, as considered in previous work of the author, this includes bisimplicial sets and Θ n -spaces.This has potential applications to the study of homotopical models for higher categories.
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.
Abstract Motivated by traces of matrices and Euler characteristics of topological spaces, we expect abstract traces in a symmetric monoidal category to be “additive”. When the category is “stable” in …
Abstract Motivated by traces of matrices and Euler characteristics of topological spaces, we expect abstract traces in a symmetric monoidal category to be “additive”. When the category is “stable” in some sense, additivity along cofiber sequences is a question about the interaction of stability and the monoidal structure. May proved such an additivity theorem when the stable structure is a triangulation, based on new axioms for monoidal triangulated categories. in this paper we use stable derivators instead, which are a different model for “stable homotopy theories”. We define and study monoidal structures on derivators, providing a context to describe the interplay between stability and monoidal structure using only ordinary category theory and universal properties. We can then perform May's proof of the additivity of traces in a closed monoidal stable derivator without needing extra axioms, as all the needed compatibility is automatic.
Homotopy limits and colimits are homotopical replacements for the usual limits and colimits of category theory, which can be approached either using classical explicit constructions or the modern abstract machinery …
Homotopy limits and colimits are homotopical replacements for the usual limits and colimits of category theory, which can be approached either using classical explicit constructions or the modern abstract machinery of derived functors. Our first goal in this paper is expository: we explain both approaches and a proof of their equivalence. Our second goal is to generalize this result to enriched categories and homotopy weighted limits, showing that the classical explicit constructions still give the right answer in the abstract sense. This result partially bridges the gap between classical homotopy theory and modern abstract homotopy theory. To do this we introduce a notion of "enriched homotopical categories", which are more general than enriched model categories, but are still a good place to do enriched homotopy theory. This demonstrates that the presence of enrichment often simplifies rather than complicates matters, and goes some way toward achieving a better understanding of "the role of homotopy in homotopy theory."
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).
Ces notes sont consacrées à la construction des limites homotopiques, et plus généralement, des images directes cohomologiques dans une catégorie de modèles arbitraire admettant des petites limites projectives. En outre, …
Ces notes sont consacrées à la construction des limites homotopiques, et plus généralement, des images directes cohomologiques dans une catégorie de modèles arbitraire admettant des petites limites projectives. En outre, la théorie des dérivateurs de Grothendieck est introduite, à la fois en tant que motivation pour l'étude de telles structures, et en tant qu'outil de démonstration.
A may bear many monoidal structures, but (to within a isomorphism) only one of category with finite products. To capture such distinctions, we consider on a 2-category those 2-monads for …
A may bear many monoidal structures, but (to within a isomorphism) only one of category with finite products. To capture such distinctions, we consider on a 2-category those 2-monads for which algebra is if it exists, giving a precise mathematical definition of essentially unique and investigating its consequences. We call such 2-monads property-like. We further consider the more restricted class of fully property-like 2-monads, consisting of those property-like 2-monads for which all 2-cells between (even lax) algebra morphisms are algebra 2-cells. The consideration of lax morphisms leads us to a new characterization of those monads, studied by Kock and Zoberlein, for which structure is adjoint to unit, and which we now call lax-idempotent 2-monads: both these and their colax-idempotent duals are fully property-like. We end by showing that (at least for finitary 2-monads) the classes of property-likes, fully property-likes, and lax-idempotents are each coreflective among all 2-monads.
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.
Abstract Traced monoidal categories are introduced, a structure theorem is proved for them, and an example is provided where the structure theorem has application.
Abstract Traced monoidal categories are introduced, a structure theorem is proved for them, and an example is provided where the structure theorem has application.
After developing the basic theory of locally cartesian localizations of presentable locally cartesian closed infinity-categories, we establish the representability of equivalences and show that univalent families, in the sense of …
After developing the basic theory of locally cartesian localizations of presentable locally cartesian closed infinity-categories, we establish the representability of equivalences and show that univalent families, in the sense of Voevodsky, form a poset isomorphic to the poset of bounded local classes, in the sense of Lurie. It follows that every infinity-topos has a hierarchy of "universal" univalent families, indexed by regular cardinals, and that n-topoi have univalent families classifying (n-2)-truncated maps. We show that univalent families are preserved (and detected) by right adjoints to locally cartesian localizations, and use this to exhibit certain canonical univalent families in infinity-quasitopoi (certain infinity-categories of "separated presheaves", introduced here). We also exhibit some more exotic examples of univalent families, illustrating that a univalent family in an n-topos need not be (n-2)-truncated, as well as some univalent families in the Morel--Voevodsky infinity-category of motivic spaces, an instance of a locally cartesian closed infinity-category which is not an n-topos for any $0\leq n\leq\infty$. Lastly, we show that any presentable locally cartesian closed infinity-category is modeled by a combinatorial type-theoretic model category, and conversely that the infinity-category underlying a combinatorial type-theoretic model category is presentable and locally cartesian closed. Under this correspondence, univalent families in presentable locally cartesian closed infinity-categories correspond to univalent fibrations in combinatorial type-theoretic model categories.
We prove two general factorization theorems for fixed-point invariants of fibrations: one for the Lefschetz number and one for the Reidemeister trace.These theorems imply the familiar multiplicativity results for the …
We prove two general factorization theorems for fixed-point invariants of fibrations: one for the Lefschetz number and one for the Reidemeister trace.These theorems imply the familiar multiplicativity results for the Lefschetz and Nielsen numbers of a fibration.Moreover, the proofs of these theorems are essentially formal, taking place in the abstract context of bicategorical traces.This makes generalizations to other contexts straightforward.
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.
We formulate differential cohomology and Chern-Weil theory -- the theory of connections on fiber bundles and of gauge fields -- abstractly in the context of a certain class of higher …
We formulate differential cohomology and Chern-Weil theory -- the theory of connections on fiber bundles and of gauge fields -- abstractly in the context of a certain class of higher toposes that we call "cohesive". Cocycles in this differential cohomology classify higher principal bundles equipped with cohesive structure (topological, smooth, synthetic differential, supergeometric, etc.) and equipped with connections, hence higher gauge fields. We discuss various models of the axioms and applications to fundamental notions and constructions in quantum field theory and string theory. In particular we show that the cohesive and differential refinement of universal characteristic cocycles constitutes a higher Chern-Weil homomorphism refined from secondary caracteristic classes to morphisms of higher moduli stacks of higher gauge fields, and at the same time constitutes extended geometric prequantization -- in the sense of extended/multi-tiered quantum field theory -- of hierarchies of higher dimensional Chern-Simons-type field theories, their higher Wess-Zumino-Witten-type boundary field theories and all further higher codimension defect field theories. We close with an outlook on the cohomological quantization of such higher boundary prequantum field theories by a kind of cohesive motives.
We introduce a new categorical framework for studying de- rived functors, and in particular for comparing composites of left and right derived functors. Our central observation is that model categories …
We introduce a new categorical framework for studying de- rived functors, and in particular for comparing composites of left and right derived functors. Our central observation is that model categories are the objects of a double category whose vertical and horizontal ar- rows are left and right Quillen functors, respectively, and that passage to derived functors is functorial at the level of this double category. The theory of conjunctions and mates in double categories, which generalizes the theory of adjunctions and mates in 2-categories, then gives us canon- ical ways to compare composites of left and right derived functors. We give a number of sample applications, most of which are improvements of existing proofs in the literature.
Working in the category T of based spaces, we give the basic theory of diagram spaces and diagram spectra. These are functorsD→T for a suitable small topological categoryD. WhenD is …
Working in the category T of based spaces, we give the basic theory of diagram spaces and diagram spectra. These are functorsD→T for a suitable small topological categoryD. WhenD is symmetric monoidal, there is a smash product that gives the category of D-spaces a symmetric monoidal structure. Examples include prespectra, as defined classically, symmetric spectra, as defined by Jeff Smith, orthogonal spectra, a coordinate-free analogue of symmetric spectra with symmetric groups replaced by orthogonal groups in the domain category, Γ-spaces, as defined by Graeme Segal, W-spaces, an analogue of Γ-spaces with finite sets replaced by finite CW complexes in the domain category. We construct and compare model structures on these categories. With the caveat that Γ-spaces are always connective, these categories, and their simplicial analogues, are Quillen equivalent and their associated homotopy categories are equivalent to the classical stable homotopy category. Monoids in these categories are (strict) ring spectra. Often the subcategories of ring spectra, module spectra over a ring spectrum, and commutative ring spectra are also model categories. When this holds, the respective categories of ring and module spectra are Quillen equivalent and thus have equivalent homotopy categories. This allows interchangeable use of these categories in applications. 2000Mathematics Subject Classification: primary 55P42; secondary 18A25, 18E30, 55U35.