9.1 Categories and precategories

In classical mathematics, there are many equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath definitions of a categoryMathworldPlanetmath. In our case, since we have dependent types, it is natural to choose the arrows to be a type family indexed by the objects. This matches the way hom-types are always used in category theoryMathworldPlanetmathPlanetmathPlanetmathPlanetmath: we never even consider comparing two arrows unless we know their domains and codomains agree. Furthermore, it seems clear that for a theory of 1-categories, the hom-types should all be sets. This leads us to the following definition.

Definition 9.1.1.

A precategory A consists of the following.

  1. 1.

    A type A0 of objects. We write a:A for a:A0.

  2. 2.

    For each a,b:A, a set homA(a,b) of arrows or morphismsMathworldPlanetmath.

  3. 3.

    For each a:A, a morphism 1a:homA(a,a).

  4. 4.

    For each a,b,c:A, a function


    denoted infix by gfgf, or sometimes simply by gf.

  5. 5.

    For each a,b:A and f:homA(a,b), we have f=1bf and f=f1a.

  6. 6.

    For each a,b,c,d:A and


    we have h(gf)=(hg)f.

The problem with the notion of precategory is that for objects a,b:A, we have two possibly-different notions of “sameness”. On the one hand, we have the type (a=A0b). But on the other hand, there is the standard categorical notion of isomorphismMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath.

Definition 9.1.2.

A morphism f:homA(a,b) is an isomorphism if there is a morphism g:homA(b,a) such that gf=1a and fg=1b. We write ab for the type of such isomorphisms.

Lemma 9.1.3.

For any f:homA(a,b), the type “f is an isomorphism” is a mere proposition. Therefore, for any a,b:A the type ab is a set.


Suppose given g:homA(b,a) and η:(1a=gf) and ϵ:(fg=1b), and similarly g, η, and ϵ. We must show (g,η,ϵ)=(g,η,ϵ). But since all hom-sets are sets, their identity types are mere propositions, so it suffices to show g=g. For this we have


using η and ϵ. ∎

If f:ab, then we write f-1 for its inverseMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath, which by \autorefct:isoprop is uniquely determined.

The only relationship between these two notions of sameness that we have in a precategory is the following.

Lemma 9.1.4 (idtoiso).

If A is a precategory and a,b:A, then


By inductionMathworldPlanetmath on identity, we may assume a and b are the same. But then we have 1a:homA(a,a), which is clearly an isomorphism. ∎

Evidently, this situation is analogous to the issue that motivated us to introduce the univalence axiom. In fact, we have the following:

Example 9.1.5.

There is a precategory Set, whose type of objects is \set, and with homSet(A,B):(AB). The identity morphisms are identity functions and the composition is function composition. For this precategory, \autorefct:idtoiso is equal to (the restrictionPlanetmathPlanetmath to sets of) the map idtoeqv from \autorefsec:compute-universe.

Of course, to be more precise we should call this category SetU, since its objects are only the small sets relative to a universePlanetmathPlanetmath U.

Thus, it is natural to make the following definition.

Definition 9.1.6.

A category is a precategory such that for all a,b:A, the function idtoisoa,b from \autorefct:idtoiso is an equivalence.

In particular, in a category, if ab, then a=b.

Example 9.1.7.

The univalence axiom implies immediately that Set is a category. One can also show, using univalence, that any precategory of set-level structuresMathworldPlanetmath such as groups, rings, topological spacesMathworldPlanetmath, etc. is a category; see \autorefsec:sip.

We also note the following.

Lemma 9.1.8.

In a category, the type of objects is a 1-type.


It suffices to show that for any a,b:A, the type a=b is a set. But a=b is equivalent to ab, which is a set. ∎

We write 𝗂𝗌𝗈𝗍𝗈𝗂𝖽 for the inverse (ab)(a=b) of the map 𝗂𝖽𝗍𝗈𝗂𝗌𝗈 from \autorefct:idtoiso. The following relationship between the two is important.

Lemma 9.1.9.

For p:a=a and q:b=b and f:homA(a,b), we have

(p,q)*(f)=𝗂𝖽𝗍𝗈𝗂𝗌𝗈(q)f𝗂𝖽𝗍𝗈𝗂𝗌𝗈(p)-1. (9.1.9)

By induction, we may assume p and q are 𝗋𝖾𝖿𝗅a and 𝗋𝖾𝖿𝗅b respectively. Then the left-hand side of (9.1.9) is simply f. But by definition, 𝗂𝖽𝗍𝗈𝗂𝗌𝗈(𝗋𝖾𝖿𝗅a) is 1a, and 𝗂𝖽𝗍𝗈𝗂𝗌𝗈(𝗋𝖾𝖿𝗅b) is 1b, so the right-hand side of (9.1.9) is 1bf1a, which is equal to f. ∎

Similarly, we can show

𝗂𝖽𝗍𝗈𝗂𝗌𝗈(p-1)=(𝗂𝖽𝗍𝗈𝗂𝗌𝗈(p))-1 (9.1.11)
𝗂𝖽𝗍𝗈𝗂𝗌𝗈(p\centerdotq)=𝗂𝖽𝗍𝗈𝗂𝗌𝗈(q)𝗂𝖽𝗍𝗈𝗂𝗌𝗈(p) (9.1.11)
𝗂𝗌𝗈𝗍𝗈𝗂𝖽(fe)=𝗂𝗌𝗈𝗍𝗈𝗂𝖽(e)\centerdot𝗂𝗌𝗈𝗍𝗈𝗂𝖽(f) (9.1.11)

and so on.

Example 9.1.11.

A precategory in which each set homA(a,b) is a mere proposition is equivalently a type A0 equipped with a mere relationMathworldPlanetmathPlanetmathPlanetmath” that is reflexiveMathworldPlanetmathPlanetmathPlanetmath (aa) and transitiveMathworldPlanetmathPlanetmathPlanetmathPlanetmath (if ab and bc, then ac). We call this a preorder.

In a preorder, a witness f:ab is an isomorphism just when there exists some witness g:ba. Thus, ab is the mere proposition that ab and ba. Therefore, a preorder A is a category just when (1) each type a=b is a mere proposition, and (2) for any a,b:A0 there exists a function (ab)(a=b). In other words, A0 must be a set, and must be antisymmetric (if ab and ba, then a=b). We call this a (partial) order or a poset.

Example 9.1.12.

If A is a category, then A0 is a set if and only if for any a,b:A0, the type ab is a mere proposition. This is equivalent to saying that every isomorphism in A is an identity; thus it is rather stronger than the classical notion of “skeletal” category. Categories of this sort are sometimes called gaunt [bsp12infncats]. There is not really any notion of “skeletality” for our categories, unless one considers \autorefct:category itself to be such.

Example 9.1.13.

For any 1-type X, there is a category with X as its type of objects and with hom(x,y):(x=y). If X is a set, we call this the discrete category on X. In general, we call it a groupoidPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath (see \autorefct:groupoids).

Example 9.1.14.

For any type X, there is a precategory with X as its type of objects and with hom(x,y):x=y0. The composition operation


is defined by induction on truncation from concatenation (y=z)(x=y)(x=z). We call this the fundamental pregroupoid of X. (In fact, we have met it already in \autorefsec:van-kampen; see also \autorefex:rezk-vankampen.)

Example 9.1.15.

There is a precategory whose type of objects is U and with hom(X,Y):XY0, and composition defined by induction on truncation from ordinary composition (YZ)(XY)(XZ). We call this the homotopyMathworldPlanetmathPlanetmath precategory of types.

Example 9.1.16.

Let Rel be the following precategory:

  • Its objects are sets.

  • homel(X,Y)=XY𝖯𝗋𝗈𝗉.

  • For a set X, we have 1X(x,x):(x=x).

  • For R:homel(X,Y) and S:homel(Y,Z), their composite is defined by


Suppose R:homRel(X,Y) is an isomorphism, with inverse S. We observe the following.

  1. 1.

    If R(x,y) and S(y,x), then (RS)(y,y), and hence y=y. Similarly, if R(x,y) and S(y,x), then x=x.

  2. 2.

    For any x, we have x=x, hence (SR)(x,x). Thus, there merely exists a y:Y such that R(x,y) and S(y,x).

  3. 3.

    Suppose R(x,y). By 2, there merely exists a y with R(x,y) and S(y,x). But then by 1, merely y=y, and hence y=y since Y is a set. Therefore, by transporting S(y,x) along this equality, we have S(y,x). In conclusionMathworldPlanetmath, R(x,y)S(y,x). Similarly, S(y,x)R(x,y).

  4. 4.

    If R(x,y) and R(x,y), then by 3, S(y,x), so that by 1, y=y. Thus, for any x there is at most one y such that R(x,y). And by 2, there merely exists such a y, hence there exists such a y.

In conclusion, if R:homRel(X,Y) is an isomorphism, then for each x:X there is exactly one y:Y such that R(x,y), and dually. Thus, there is a function f:XY sending each x to this y, which is an equivalence; hence X=Y. With a little more work, we conclude that Rel is a category.

We might now restrict ourselves to considering categories rather than precategories. Instead, we will develop many concepts for precategories as well as categories, in order to emphasize how much better-behaved categories are, as compared both to precategories and to ordinary categories in classical mathematics.

We will also see in \crefrangesec:strict-categoriessec:dagger-categories that in slightly more exotic contexts, there are uses for certain kinds of precategories other than categories, each of which “fixes” the equality of objects in different ways. This emphasizes the “pre”-ness of precategories: they are the raw material out of which multiple important categorical structures can be defined.

Title 9.1 Categories and precategories