Introduction

The goal of this book is to establish an axiomatic framework for higher category theory. This approach is best thought of as a form of synthetic category theory: instead of constructing higher categories from more primitive objects, the axioms impose the intended behavior of higher categories directly. This stands in contrast to analytic approaches, such as the theory of quasicategories, in which one first constructs higher categories inside a background foundation, typically set theory, and then proves that the resulting objects have the desired categorical properties.

Mathematical motivation

Category theory has long been a useful unifying language for abstract mathematics. Higher category theory¹ refines ordinary category theory by allowing all constructions and properties to be considered up to coherent homotopy. In recent decades, higher category theory and homotopy theory have become central tools in algebraic topology, algebraic geometry, representation theory, mathematical physics, and many other fields.

Footnote 1

¹More specifically: \((\infty ,1)\)-category theory.

Return to text

The traditional foundations of the field have rested on specific models, most notably the framework of quasicategories developed by Joyal [Joy08] and Lurie [Lur09; Lur17]. As the subject matured, however, it became clear that most of its results and constructions are model-independent: they never touch the combinatorial details of quasicategories, or of any other model. One way to say this is that there is a language of category theory, of which the classical set-based notion, a category as a set of objects and a set of morphisms, is one interpretation, and the theory of quasicategories another. The working content of higher category theory lives in the language, not in any single interpretation of it. Following this viewpoint, much recent work is written in a deliberately model-agnostic style that avoids the combinatorial scaffolding of quasicategories.

One primary goal of this book is to provide a detailed account of this model-independent language of category theory, and to identify a list of key categorical axioms one needs to assume to build up the rest of the theory. We believe this allows for a more direct and intuitive engagement with the core concepts of higher category theory, and that it leads to proofs carrying insights that may have been obscured by model-specific details in more traditional treatments of the theory.

Our framework has three further advantages:

Parametrized \(\infty \)-category theory: Our formalism is designed to serve as the internal language of the \(\infty \)-category of sheaves of \(\infty \)-categories on any \(\infty \)-topos. Thus all results proved in this book are automatically valid in parametrized category theory, as in the work of Barwick et al. [Bar+16] on genuine equivariant homotopy theory and the work of Martini and Wolf [MW24] on category theory internal to an \(\infty \)-topos.
A working language for \(\infty \)-category theory: The theory specifies the basic notions, operations, and identifications in a language in which one can teach and use \(\infty \)-category theory in the same way one uses naive set theory, making the subject more accessible.
Elementary \(\infty \)-category theory: The axioms are constructive, and hence shed light on the scope of “elementary \(\infty \)-category theory”: Even constructively it is possible to recover substantial parts of standard higher category theory.

An alternative formal approach to higher category theory was developed by Riehl and Verity [RV22]. Their \(\infty \)-cosmoi are certain categories enriched in quasicategories and make systematic use of cotensors by simplicial sets. Their work is model-independent in the sense that a common formalism applies to any \(\infty \)-cosmos satisfying suitable axioms. Our aim is different: the language developed here is model-agnostic, in that it does not refer to a model of higher categories at all.

Philosophical motivation

There is also a philosophical reason to formalize higher category theory: category theory can serve as a foundation for mathematics. This idea goes back at least to Lawvere, and it has been developed in many forms since then; see for instance Landry and Marquis [LM05] for historical context.

The point of view in this book is that categories, in fact \((\infty ,1)\)-categories, should be treated as the building blocks of mathematics, in the role traditionally played by sets or types. One way to study mathematical objects within category theory is through the categories they form; this perspective is already a common practice in fields like algebraic geometry and algebraic topology. We wish to highlight a second way to recover ordinary mathematics as a fragment of the theory of categories: by first restricting the theory to animae, those categories in which every morphism is an isomorphism, and then further to sets, those animae that admit at most one isomorphism between every two objects. The resulting set theory can then be used to define other mathematical objects in the usual way.

The latter perspective also makes clear that the jump from set-based mathematics to category-based mathematics consists of two conceptual leaps, corresponding to the passage from sets to animae and the passage from animae to categories.

The first leap concerns the notion of equality. In set-based mathematics, equality is treated as a property: two elements of a set are either equal or they are not, and there is no further question of how they are equal. In anima-based mathematics, equality is instead treated as an intrinsic structure. To illustrate the difference, set-based mathematics treats two abelian groups as the same if they are strictly equal as sets with equal operations, while the anima-based perspective on such equalities would amount to group isomorphisms. The structured perspective on equality is not new; for example:

Makkai [Mak98] proposed the Principle of Isomorphism: All grammatically correct properties of objects of a category are to be invariant under isomorphism.
Voevodsky’s homotopy type theory (HoTT) [Uni13] builds in a flexible notion of equality which has the key feature that it is compatible with the Univalence Axiom, which roughly states that two isomorphic types (groups, topological spaces, etcetera) are equal to each other.

We take it as our main guiding principle throughout the book:

Fundamental Principle of Homotopy Theory: When expressing that two entities are equal, we must always specify how they are equal by providing an isomorphism between them. All valid mathematical constructions should preserve these isomorphisms.

Taking this principle seriously, we are forced to replace sets as our basic notion of ‘collections of mathematical objects’: equality in sets is too rigid. The new fundamental object in this paradigm is called an anima, which may be described as a collection of objects such that for each two objects there is an anima of isomorphisms between them. This gives animae the structure of a groupoid. By considering equality of morphisms, we also have isomorphisms between isomorphisms, and repeating this process we see that animae naturally behave like \(\infty \)-groupoids. Other common names in the literature are spaces or homotopy types; HoTT for example uses the latter framing. In this book, however, the word space is reserved for an actual topological space.

The second leap is to replace animae by categories as the primitive building blocks of the theory. In practice, a class of mathematical objects often naturally comes with more general relations between objects than mere isomorphisms; think of homomorphisms between groups, continuous maps between topological spaces, functors between categories. The concept of a category encapsulates this by encoding morphisms between objects and behavior of their compositions.

The classical perspective on categories is analytic: a category consists of a set of objects and a set of morphisms, satisfying various axioms. This perspective clashes with Makkai’s principle of isomorphism, as it allows one to distinguish two isomorphic objects: categories should have an anima of objects and a anima of morphisms. In light of this, it may be tempting to try to define categories directly within HoTT. However, we argue that it is better to make a second leap, and directly take categories to be the primitive objects of the theory, with sets and animae arising as special cases.

Just like the fundamental principle of homotopy theory forces animae to behave like \(\infty \)-groupoids, it also forces categories to behave like \((\infty ,1)\)-categories: equality between morphisms must be encoded by some notion of 2-isomorphisms, equality between those by 3-isomorphisms, and so on. In this way, the language of category theory natively speaks about \((\infty ,1)\)-categories, and strict 1-categories are merely a fragment of this theory.

For broader discussions of categorical and structural foundations of mathematics, we refer to Tsementzis [Tse17], Marquis [Mar13], Rodin [Rod14], and Awodey [Awo14].

Synthetic category theory eats itself

One of the distinctive features of synthetic category theory is that it can interpret itself. We take this as a key design criterion: There should be a universe \(\Cat \) whose objects are small synthetic categories, and all the axioms of the theory we develop should ultimately be satisfied in the internal language of \(\Cat \). In this sense, it is analogous to the role of Grothendieck universes in set theory: sets large enough to contain the usual set-theoretic constructions, which can therefore serve as a model of set theory inside set theory. A systematic verification of this design criterion is deferred to Volume II.

The axiom that makes this precise is directed univalence, which relates morphisms in \(\Cat \) to functors between synthetic categories. The main consequence of this axiom is the familiar Grothendieck correspondence: for every small synthetic category \(C\), functors \[ C \to \Cat \] correspond to small cocartesian fibrations over \(C\). To illustrate why this relates the external theory of synthetic categories to the internal theory of \(\Cat \), it is illustrative to consider the terminal case \(C = *\). In this case, the Grothendieck correspondence says that objects of \(\Cat \) correspond to small cocartesian fibrations over the terminal category, hence to small synthetic categories. Applying the principle to more general instances of \(C\) then provides the translation between the internal language of \(\Cat \) and the external language of categories that we are setting up.

Restricting directed univalence to animae recovers Voevodsky’s univalence axiom: isomorphisms between animae correspond to equalities in the subuniverse \(\An \subseteq \Cat \) of animae. But the directed form is stronger: it also says that maps between animae correspond to morphisms in \(\An \). This also marks a crucial difference with homotopy type theory: HoTT has a universe of types, and univalence explains equality in that universe, but this does not yet give a self-interpretation of HoTT inside HoTT. The problem is to internalize the syntax of type theory together with its higher coherence in plain homotopy type theory. Synthetic category theory is designed so that the theory eats itself: the universe \(\Cat \) should serve not only as one object of the theory, but also as a semantic universe in which the theory can be interpreted. This model theorem will be developed in Volume II.

Relation to type theory

In this book, we present the theory of synthetic categories in ordinary mathematical language, specifying its basic notions, operations, and coherence identifications. The main objective of this book is to provide a model-agnostic presentation of synthetic category theory, and build up standard category theory from a sizable list of foundational axioms. No knowledge of type theory is required to read this book.

Nevertheless, our work is heavily inspired by type-theoretic considerations, and we expect it to be possible to write down rigorous type-theoretic syntax and derivation rules that allow the theory to be formalized in proof assistants. We are exploring several approaches:

A presentation of the theory à la Martin-Löf is in preparation in collaboration with Michele Riva;
A presentation of the theory within the type theory CaTT of \(\omega \)-categories [FM17; BFM24] is in preparation in collaboration with Ivan Kobe.

For readers familiar with dependent type theory, we wish to flag two differences with synthetic category theory.

The first difference concerns the Curry–Howard correspondence: the idea that types may be interpreted as mathematical statements, and terms of a type as proofs of those statements. Constructions of types, like the disjoint union \(X \sqcup Y\) or the product \(X \times Y\), then admit logical interpretations, like the logical disjunction \(P \lor Q\) and logical conjunction \(P \land Q\). Under this correspondence, propositions appear as the special case of \((-1)\)-truncated types: those types which admit at most one term.

In synthetic category theory, it is no longer the case that arbitrary types correspond to mathematical statements. General types are now interpreted as categories, which allow for non-invertible maps between objects. The types corresponding to statements are the primitive animae, which the groupoid recognition axiom identifies with the categories in which every morphism is an isomorphism.

The second difference concerns type dependency. In ordinary dependent type theory, for each context \(\Gamma \), the types in context \(\Gamma \) form a category, and any substitution \[ f\colon \Delta \to \Gamma \] induces a pullback operation on types. This pullback operation preserves the logical structure of the theory: products, sums, identity types, and the other type-forming operations are stable under substitution. In this sense, substitution along an arbitrary map of contexts preserves the logic.

In synthetic category theory, this principle breaks in a controlled way. It continues to behave as expected when the contexts involved are animae. But if \(\Gamma \) is a general synthetic category, then a type in context \(\Gamma \) should be thought of as a category over \(\Gamma \), that is, as a functor \[ p\colon X \to \Gamma . \] The resulting theory of categories over \(\Gamma \) is not, in general, again a semantic interpretation of synthetic category theory.

However, there is a better category-theoretic replacement: among functors \(X \to \Gamma \), one should restrict to cocartesian fibrations over \(\Gamma \). The resulting category does form a semantic interpretation of synthetic category theory. This theory is not equivalent to the naive theory of all categories over \(\Gamma \), except when \(\Gamma \) is an anima. A precise form of this result is treated in Volume II.

Still, even when we restrict to cocartesian fibrations, pullback along an arbitrary functor \(f\colon \Delta \to \Gamma \) does not generally preserve all categorical structure: unlike in type theory, substitution does not fully preserve the logic.

We wish to regard this phenomenon as a feature rather than a bug: It is one of the ways in which synthetic category theory is more expressive than ordinary dependent type theory. The comparison between the naive theory of categories over \(\Gamma \) and the theory of cocartesian fibrations over \(\Gamma \) is itself structured: it is governed by adjunctions and by canonical comparison maps, many of which are not invertible. Such non-invertible comparison maps are not pathological in category theory: they often form an integral part of the mathematical discourse of the subject.

Consistency

The consistency of the theory presented in this book is controlled by the usual models of higher category theory. Cisinski’s work on higher categories [Cis19], together with the work of Cisinski and Nguyen on the universal cocartesian fibration [CN22], shows that Joyal’s theory of quasicategories gives a semantic interpretation of synthetic category theory. Thus the theory is at least as consistent as the usual set-theoretic foundations used to construct quasicategories.

Let us note that the proof of directed univalence, namely the fact that there is a reasonable \(\infty \)-category of \(\infty \)-categories, subsumes Voevodsky’s proof of the univalence axiom for Kan complexes [KL21].

As mentioned before, the work of Buchholtz, Gratzer and Weinberger [GWB26] on simplicial type theory is expected to provide a constructive semantic interpretation of synthetic category theory within the framework of Riehl and Shulman [RS17]. Conversely, the present book proves among other things that the synthetic category of synthetic categories is equivalent to the synthetic category of univalent Segal objects in animae, which can be used as the basis for an internal version of simplicial homotopy type theory. This indicates that synthetic category theory and simplicial type theory are mutually consistent, constructively.

Organization of the book

The present version of the book is organized as follows:

(1): In Chapter 1, we introduce the language of synthetic category theory. Categories, animae, functors and isomorphism animae between functors are taken as primitive, and all our axioms are expressed in terms of them. We introduce products, coproducts, pullbacks and functor categories via universal properties, and use mapping animae to define the collection of objects of a category.
(2): In Chapter 2, we study the internal structure of categories. We introduce morphisms and commutative diagrams, and formulate the Segal axiom and the Rezk axiom to ensure that the objects we call synthetic categories do indeed behave like categories. We then relate primitive animae to the structural notion of a groupoid and study groupoid cores. Animae play a fundamental role in our approach: an object of a synthetic category \(C\) is a functor \(x\colon \Gamma \to C\) whose source is allowed to be an arbitrary anima \(\Gamma \).
(3): In Chapter 3, we introduce various fundamental categorical constructions in the setting of synthetic category theory: full subcategories, localizations, geometric realizations, relative functor categories, joins and slices.
(4): In Chapter 4 (outside selection), we develop the language of categories over a context, terms as sections, reindexing, and context extension. The theory developed in this book remains valid for categories in an anima context. Some results even work in arbitrary categorical contexts; we distinguish those by underlining them.
(5): In Chapter 5 (outside selection), we introduce adjunctions, initial and terminal objects, limits and colimits, left and right fibrations, and cartesian and cocartesian fibrations, among other things. We also introduce the Functoriality of universals axiom, which states that in order to provide a left adjoint section to a cartesian fibration \(p\colon E \to C\) it is enough to show that all the fibers of \(p\) admit initial objects.
(6): One of the most fundamental theorems in category theory is the fact that a functor is an equivalence if and only if it is fully faithful and strongly surjective. We prove this result in Chapter 6 (outside selection).
(7): The main goal of Chapter 7 (outside selection) is to axiomatize a synthetic category \(\Cat \) of small synthetic categories. It comes equipped with a cocartesian fibration \(\pi _{\univ }\colon \Cat _{\bullet } \to \Cat \) satisfying the property that for every small synthetic category \(C\) there is an equivalence between functors from \(C\) to \(\Cat \) and cocartesian fibrations over \(C\) with small fibers. The equivalence is given by pulling back the universal small cocartesian fibration \(\pi _{\univ }\) along the given functor \(C \to \Cat \).
(8): Chapter 8 (outside selection) studies initial and terminal functors, proper and smooth functors, weak homotopy equivalences, and base change.
(9): Chapter 11 (outside selection) develops opposite categories, twisted arrow categories, the Yoneda lemma, representable approximation, locally small categories, and descent.
(10): Chapter 9 (outside selection) develops sets, natural numbers, simplices, covers, truncation.
(11): Chapter 10 (outside selection) introduces covers and truncation, thus opening the possibility of dealing constructively with mere existence statements. We also discuss sets and posets.
(12): Chapter 12 (outside selection) free completions by small colimits and descent. In particular, Quillen’s theorem B is proven.
(13): Chapter 13 (outside selection) studies products in localizations, localizations and adjunctions, and the calculus of fractions.
(14): Chapter 14 (outside selection) explains how univalent Segal animae and the Rezk nerve functor yield a new description of the universe of categories.
(15): Chapter 15 (outside selection) develops filtered categories and filtered colimits of animae, together with the theory of finite categories.
(16): Chapter 16 (outside selection) studies left or right exact localizations as well as presentable categories with respect to a fixed universe (later in the book, this will specialize to finite posets or finite sets, for instance).
(17): Chapter 17 (outside selection) studies compact generation, tensor product of finitely cocomplete categories, and Ind-objects.
(18): Chapter 18 (outside selection) develops finite-colimit completions, stable categories, spectra, and Verdier quotients.
(19): Chapter 19 (outside selection) develops additive and Waldhausen categories, completions by sifted colimits, the \(S\)-construction, additivity, the universal property of \(K\)-theory (and of the waldhausen \(S\)-construction in general), and the localization theorem in algebraic K-theory.
(20): Chapter 20 (outside selection) introduces a new accessibility axiom and develops the theory of presentable categories in full generality - existence of left Bousfield locazitions, presentation as left Bousfield localizations of categories of presheaves, adjoint functor theorem.