9. Category theory

Of the branches of mathematics, category theory is one which perhaps fits the least comfortably in set theoretic foundations. One problem is that most of category theory is invariant under weaker notions of “sameness” than equality, such as isomorphism in a category or equivalence of categories, in a way which set theory fails to capture. But this is the same sort of problem that the univalence axiom solves for types, by identifying equality with equivalence. Thus, in univalent foundations it makes sense to consider a notion of “category” in which equality of objects is identified with isomorphism in a similar way.

Ignoring size issues, in set-based mathematics a category consists of a set $A_0$ of objects and, for each $x,y\in A_0$, a set ${\mathrm{hom}}_A(x,y)$ of morphisms. Under univalent foundations, a “naive” definition of category would simply mimic this with a type of objects and types of morphisms. If we allowed these types to contain arbitrary higher homotopy, then we ought to impose higher coherence conditions, leading to some notion of $(\mathrm{\infty },1)$-category, but at present our goal is more modest. We consider only 1-categories, and therefore we restrict the types ${\mathrm{hom}}_A(x,y)$ to be sets, i.e. 0-types. If we impose no further conditions, we will call this notion a precategory.

If we add the requirement that the type $A_0$ of objects is a set, then we end up with a definition that behaves much like the traditional set-theoretic one. Following Toby Bartels, we call this notion a strict category. But we can also require a generalized version of the univalence axiom, identifying $(x{=}_{A_0}y)$ with the type $\mathrm{𝗂𝗌𝗈}(x,y)$ of isomorphisms from $x$ to $y$. Since we regard this as usually the “correct” definition, we will call it simply a category.

A good example of the difference between the three notions of category is provided by the statement “every fully faithful and essentially surjective functor is an equivalence of categories”, which in classical set-based category theory is equivalent to the axiom of choice.

1. For strict categories, this is still equivalent to the axiom of choice.

2. For precategories, there is no consistent axiom of choice which can make it true.

3. For categories, it is provable without any axiom of choice.

We will prove the latter statement in this chapter, as well as other pleasant properties of categories, e.g. that equivalent categories are equal (as elements of the type of categories). We will also describe a universal way of “saturating” a precategory $A$ into a category $\widehat{A}$, which we call its Rezk completion, although it could also reasonably be called the stack completion (see the Notes).

The Rezk completion also sheds further light on the notion of equivalence of categories. For instance, the functor $A\to \widehat{A}$ is always fully faithful and essentially surjective, hence a “weak equivalence”. It follows that a precategory is a category exactly when it “sees” all fully faithful and essentially surjective functors as equivalences; thus our notion of “category” is already inherent in the notion of “fully faithful and essentially surjective functor”.

We assume the reader has some basic familiarity with classical category theory. Recall that whenever we write $𝒰$ it denotes some universe of types, but perhaps a different one at different times; everything we say remains true for any consistent choice of universe levels. We will use the basic notions of homotopy type theory from cha:typetheory,cha:basics and the propositional truncation from cha:logic, but not much else from part:foundations, except that our second construction of the Rezk completion will use a higher inductive type.

Title	9. Category theory