Overview of the axioms

Overview of the axioms

The axioms are introduced progressively, since several require preliminary categorical language before they can be stated. This chapter gives a concise overview of the actual axiomatic package and the principal constructions used in its formulation. Precise statements and dependencies appear in the chapters that follow.

The language of synthetic category theory

Synthetic category theory rests upon a language of categories, functors and identifications, together with specified operations and coherences. We will now provide a rough overview of this language, leaving the details to Chapter 1.

Animae serve as the homotopy-coherent collections of the theory, playing the role of sets in ordinary mathematics. The distinguishing feature is the notion of equality in an anima: given two identifications \(p,q : x =_X y\), we may talk about identifications between \(p\) and \(q\), and this process may be iterated. This also applies to identifications between functors.

A functor \(f\colon C\to D\) may be displayed in term notation as \(x:C\vdash f(x):D\). Substitution displays composition of functors; identifications of expressions are identifications of the whole functors.

A functor \(f\colon C \to D\) is said to be an equivalence if there exists another functor \(g\colon D \to C\) and identifications \(\id _{C} = gf\) and \(\id _D = fg\).

There are various ways to build new categories out of old ones. In each case, we will specify the behavior of these constructions by prescribing how to define functors into/out of them and how to define identifications between functors into/out of them. We record only the coherence data and relations used explicitly in the development.

We define the collection of objects in a category \(C\) to be \(C^\simeq =\Map (*,C)\). We define an absolute object of a category \(C\) to be a functor \(x\colon * \to C\).

The internal structure of categories

We now turn to morphisms and their composition, developed in Chapter 2. To speak of morphisms, we need another axiom:

We may then define a morphism in \(C\) to be a functor \(f\colon [1] \to C\). We refer to the objects \(f(0)\) and \(f(1)\) of \(C\) as the source and target of \(f\), respectively, and often write \(f\colon x \to y\) to indicate that \(f\) comes equipped with identifications \(x = f(0)\) and \(y = f(1)\). Similarly, a natural transformation of functors \(C \to D\) is defined as a functor \(C \times [1] \to D\), or equivalently a functor \(C \to \Fun ([1],D)\).

The walking commutative triangle is the category \([2] := \Fun ([1],[1])\). It comes with objects \(0\), \(1\) and \(2\), and with functors \(d_0,d_1,d_2\colon [1] \to [2]\) and \(s_0,s_1\colon [2] \to [1]\) satisfying the simplicial identities. A commutative triangle in \(C\) is a functor \([2] \to C\), and a commutative square is a functor \([1] \times [1] \to C\). Every commutative square determines two commutative triangles by precomposition with the maps \(j_0 := (s_0,s_1)\colon [2] \to [1] \times [1]\) and \(j_1 := (s_1,s_0)\colon [2] \to [1] \times [1]\), and we demand that the original square can be uniquely recovered from this data:

Every object \(x\colon * \to C\) gives rise to an identity morphism \(\id _x\colon x \to x\), defined as the composite \([1] \xrightarrow {p_{[1]}} * \xrightarrow {x} C\). The definition of composition of morphisms in \(C\) requires another axiom:

Given morphisms \(f\colon x \to y\) and \(g\colon y \to z\), the axiom provides a unique commutative triangle \(\sigma \colon [2]\to C\) satisfying \(d_2^*(\sigma ) = f\) and \(d_0^*(\sigma ) = g\). The resulting morphism \(g \circ f := d_1^*(\sigma )\colon [1] \to C\) is called the composite of \(f\) and \(g\). One can prove that composition of morphisms is automatically unital and associative.

Having both identity morphisms and composition, we may now introduce the notion of isomorphism in \(C\): a morphism \(f\colon x \to y\) in \(C\) is an isomorphism if it admits a left inverse \(g\colon y \to x\) (satisfying \(gf = \id _x\)) as well as a right inverse \(h\colon y \to x\) (satisfying \(fh = \id _y\)). Using diagram categories, we may in fact construct for every \(C\) a category \(\Iso (C)\) whose objects are precisely the isomorphisms in \(C\) (equipped with the data of left and right inverses). The canonical example of an isomorphism in \(C\) is the identity morphism \(\id _x\colon x \to x\), in which case the left and right inverses are simply \(\id _x\) itself. This construction provides a functor \(i\colon C \to \Iso (C)\), which we demand to be an equivalence:

Axioms E and F are inspired by Rezk’s notion of complete Segal spaces.

We now introduce the following recognotion principle for animae.

Constructions of categories

Equipped with a basic language of categories, functors and identifications, we can start formulating our remaining axioms of category theory. We first recall the groupoid cores of categories. Using the above notion of isomorphisms in a category \(C\), we say that \(C\) is a groupoid if all of its morphisms are isomorphisms.

For every category \(C\), there is an anima \(C^{\simeq }\) called the groupoid core of \(C\), equipped with a functor \(\imath _C \colon C^{\simeq } \to C\) simply defined as \[ C^\simeq =\Map (*,C)\, . \] Every functor \(f\colon X \to C\) from an anima \(X\) factors through \(\imath _C\), and for functors \(g,h\colon X \to C^{\simeq }\) every identification \(\imath _C \circ g = \imath _C \circ h\) may be lifted to an identification \(g = h\).

For categories \(C\) and \(D\), the primitive mapping anima \(\Map (C,D)\) is related to the functor category by a preferred equivalence \[ \Map (C,D)\simeq \Fun (C,D)^{\simeq }. \]

We also demand the existence of subcategories, localizations, geometric realizations and joins, discussed in detail in Chapter 3:

In the case where \(W\) consists of all morphisms in \(C\), we denote the localization by \(\geom {C}\) and call it the geometric realization of \(C\). It is automatically an anima.

Axiom J (Join axioms). For every category \(\Gamma \) and functors \(C\to \Gamma \) and \(D\to \Gamma \), there is a relative join \(C\star _\Gamma D\to \Gamma \). If \[ j_\Gamma :=\id _\Gamma \times j\colon \Gamma \times \partial [1]\longrightarrow \Gamma \times [1] \] is the weakening of the boundary inclusion, then the height functor \(h_{C,D}\colon C\star _\Gamma D\to \Gamma \times [1]\) is a dependent product of \(C\sqcup D\) over \(\Gamma \times \partial [1]\) along \(j_\Gamma \).

When \(\Gamma \) is an anima, the relative join also satisfies the mapping-out exactness property: it is exhibited by a pushout square

The absolute join \(C\star D\) is the special case \(\Gamma = *\).

If we write \([0]\) for the terminal category \(*\), we have \([1] \iso [0] \star [0]\), and we may inductively define \([n + 1] := [n] \star [0]\).

Cartesian and cocartesian fibrations

An important concept in category theory is that of a cocartesian fibration: a functor \(E \to C\) whose fibers \(E_c\) vary covariantly and functorially in the object \(c \in C\). In Chapter 5 (outside selection), we introduce a synthetic analogue of this definition: a functor \(f\colon A \to B\) is called a cocartesian fibration if a certain ‘directed evaluation map’ \(\vec {\ev }^f_0\colon \Fun ([1], A) \to A \vectimes {f} B\) admits a left adjoint section \(\lift ^f_0\colon A \vectimes {f} B \to \Fun ([1],A)\). Informally, this left adjoint section provides the cocartesian lifts \(a \to \beta _!(a)\) in \(A\) for morphisms \(\beta \colon b \to b'\) in \(B\) with specified lift \(a\) of \(b\). One may dually define cartesian fibrations.

Given a cocartesian fibration \(p\colon U_{\bullet } \to U\), one can formulate what it means for \(p\) to satisfy directed univalence: roughly speaking, this means that for functors \(f_0,f_1\colon C \to U\) with pullback fibrations \(E_i := f_i^*(U_{\bullet }) \to C\), the anima of natural transformations \(\alpha \colon f_0 \to f_1\) is equivalent to the anima of cocartesian functors \(E_0 \to E_1\) over \(C\). This condition will in particular imply a form of straightening/unstraightening. A category \(U\) equipped with such a univalent cocartesian fibration \(p\) is called a universe. We say that \(U\) is a universe of categories if it is closed under all the categorical operations introduced so far; see Definition 7.4.5 (outside selection) for a complete list.

We will usually fix a universe of categories \(\pi _{\univ }\colon \Cat _{\bullet } \to \Cat \) and work with categories that are small with respect to this universe, i.e. those categories \(C\) that can be obtained from an object \(c\) of \(\Cat \) via the following pullback square:

A consequence of directed univalence is the straightening/unstraightening equivalence \[ \Un \colon \Fun (C,\Cat )\iso \CoCart (C) \] for every small category \(C\). Here \(\CoCart (C)\) is the subcategory of the slice category \(\Cat _{/C}\) whose objects are small cocartesian fibrations over \(C\) and whose morphisms are cocartesian functors. This correspondence motivates the intended interpretation of synthetic category theory in the universe \(\Cat \); its systematic verification belongs to Volume II.