9. Category theory

Of the branches of mathematics, category theoryMathworldPlanetmathPlanetmathPlanetmathPlanetmath 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 isomorphismMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath in a categoryMathworldPlanetmath or equivalence of categories, in a way which set theoryMathworldPlanetmath 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 A0 of objects and, for each x,yA0, a set homA(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 (,1)-category, but at present our goal is more modest. We consider only 1-categories, and therefore we restrict the types homA(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 A0 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=A0y) with the type 𝗂𝗌𝗈(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 differencePlanetmathPlanetmath between the three notions of category is provided by the statement “every fully faithfulPlanetmathPlanetmath and essentially surjective functor is an equivalence of categories”, which in classical set-based category theory is equivalentMathworldPlanetmathPlanetmathPlanetmath to the axiom of choiceMathworldPlanetmath.

  1. 1.

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

  2. 2.

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

  3. 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 universalPlanetmathPlanetmathPlanetmath way of “saturating” a precategory A into a category 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 functorMathworldPlanetmath AA^ is always fully faithful and essentially surjective, hence a “weak equivalenceMathworldPlanetmath”. 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 universePlanetmathPlanetmath 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 \autorefcha:typetheory,\autorefcha:basics and the propositional truncation from \autorefcha:logic, but not much else from \autorefpart:foundations, except that our second construction of the Rezk completion will use a higher inductive type.

Title 9. Category theory