9.1 Categories and precategories

In classical mathematics, there are many equivalent definitions of a category. 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 theory: 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.

A type $A_{0}$ of objects. We write $a : A$ for $a:A_{0}$ .
2.

For each $a, b : A$ , a set $\hom_{A}(a,b)$ of arrows or morphisms.
3.

For each $a : A$ , a morphism $1_{a}:\hom_{A}(a,a)$ .
4.

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

$\hom_{A}(b,c)\to\hom_{A}(a,b)\to\hom_{A}(a,c)$

denoted infix by $g\mapsto f\mapsto g\circ f$ , or sometimes simply by $g f$ .
5.

For each $a, b : A$ and $f:\hom_{A}(a,b)$ , we have $f=1_{b}\circ f$ and $f=f\circ 1_{a}$ .
6.

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

$f:\hom_{A}(a,b),\qquad g:\hom_{A}(b,c),\qquad h:\hom_{A}(c,d),$

we have $h\circ(g\circ f)=(h\circ g)\circ 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=_{A_{0}}b)$ . But on the other hand, there is the standard categorical notion of isomorphism.

Definition 9.1.2.

A morphism $f:\hom_{A}(a,b)$ is an isomorphism if there is a morphism $g:\hom_{A}(b,a)$ such that $g\circ f=1_{a}$ and $f\circ g=1_{b}$ . We write $a\cong b$ for the type of such isomorphisms.

Lemma 9.1.3.

For any $f:\hom_{A}(a,b)$ , the type “ $f$ is an isomorphism” is a mere proposition. Therefore, for any $a, b : A$ the type $a\cong b$ is a set.

Proof.

Suppose given $g:\hom_{A}(b,a)$ and $\eta:(1_{a}=g\circ f)$ and $\epsilon:(f\circ g=1_{b})$ , and similarly $g^{\prime}$ , $\eta^{\prime}$ , and $\epsilon^{\prime}$ . We must show $(g,\eta,\epsilon)=(g^{\prime},\eta^{\prime},\epsilon^{\prime})$ . But since all hom-sets are sets, their identity types are mere propositions, so it suffices to show $g=g^{\prime}$ . For this we have

g^{\prime}=1_{a}\circ g^{\prime}=(g\circ f)\circ g^{\prime}=g\circ(f\circ g^{% \prime})=g\circ 1_{b}=g

using $\eta$ and $\epsilon^{\prime}$ . ∎

If $f:a\cong b$ , then we write ${f}^{-1}$ for its inverse, 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

(a=b)\to(a\cong b).

Proof.

By induction on identity, we may assume $a$ and $b$ are the same. But then we have $1_{a}:\hom_{A}(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 $\mathcal{S}et$ , whose type of objects is \set, and with $\hom_{\mathcal{S}et}(A,B):\!\!\equiv(A\to B)$ . The identity morphisms are identity functions and the composition is function composition. For this precategory, \autorefct:idtoiso is equal to (the restriction to sets of) the map $\mathsf{idtoeqv}$ from \autorefsec:compute-universe.

Of course, to be more precise we should call this category $\mathcal{S}et_{\mathcal{U}}$ , since its objects are only the small sets relative to a universe $\mathcal{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 $\mathsf{idtoiso}_{a,b}$ from \autorefct:idtoiso is an equivalence.

In particular, in a category, if $a\cong b$ , then $a=b$ .

Example 9.1.7.

The univalence axiom implies immediately that $\mathcal{S}et$ is a category. One can also show, using univalence, that any precategory of set-level structures such as groups, rings, topological spaces, 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.

Proof.

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

We write $\mathsf{isotoid}$ for the inverse $(a\cong b)\to(a=b)$ of the map $\mathsf{idtoiso}$ from \autorefct:idtoiso. The following relationship between the two is important.

Lemma 9.1.9.

For $p:a=a^{\prime}$ and $q:b=b^{\prime}$ and $f:\hom_{A}(a,b)$ , we have

{(p,q)}_{*}\mathopen{}\left({f}\right)\mathclose{}=\mathsf{idtoiso}(q)\circ f% \circ{\mathsf{idtoiso}(p)}^{-1}.

(9.1.9)

Proof.

By induction, we may assume $p$ and $q$ are $\mathsf{refl}_{a}$ and $\mathsf{refl}_{b}$ respectively. Then the left-hand side of (9.1.9) is simply $f$ . But by definition, $\mathsf{idtoiso}(\mathsf{refl}_{a})$ is $1_{a}$ , and $\mathsf{idtoiso}(\mathsf{refl}_{b})$ is $1_{b}$ , so the right-hand side of (9.1.9) is $1_{b}\circ f\circ 1_{a}$ , which is equal to $f$ . ∎

Similarly, we can show

	$\displaystyle\mathsf{idtoiso}(\mathord{{p}^{-1}})={(\mathsf{idtoiso}(p))}^{-1}$		(9.1.11)
	$\displaystyle\mathsf{idtoiso}(p\mathchoice{\mathbin{\raisebox{2.15pt}{$% \displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{% \mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox% {0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}q)=\mathsf{idtoiso}(q)\circ% \mathsf{idtoiso}(p)$		(9.1.11)
	$\displaystyle\mathsf{isotoid}(f\circ e)=\mathsf{isotoid}(e)\mathchoice{% \mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{\raisebox{2.1% 5pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}% }}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}\mathsf{% isotoid}(f)$		(9.1.11)

and so on.

Example 9.1.11.

A precategory in which each set $\hom_{A}(a,b)$ is a mere proposition is equivalently a type $A_{0}$ equipped with a mere relation “ $\leq$ ” that is reflexive ( $a\leq a$ ) and transitive (if $a\leq b$ and $b\leq c$ , then $a\leq c$ ). We call this a preorder.

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

Example 9.1.12.

If $A$ is a category, then $A_{0}$ is a set if and only if for any $a,b:A_{0}$ , the type $a\cong b$ 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):\!\!\equiv(x=y)$ . If $X$ is a set, we call this the discrete category on $X$ . In general, we call it a groupoid (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):\!\!\equiv\mathopen{}\left\|x=y\right\|_{0}\mathclose{}$ . The composition operation

\mathopen{}\left\|y=z\right\|_{0}\mathclose{}\to\mathopen{}\left\|x=y\right\|_% {0}\mathclose{}\to\mathopen{}\left\|x=z\right\|_{0}\mathclose{}

is defined by induction on truncation from concatenation $(y=z)\to(x=y)\to(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 $\mathcal{U}$ and with $\hom(X,Y):\!\!\equiv\mathopen{}\left\|X\to Y\right\|_{0}\mathclose{}$ , and composition defined by induction on truncation from ordinary composition $(Y\to Z)\to(X\to Y)\to(X\to Z)$ . We call this the homotopy precategory of types.

Example 9.1.16.

Let $\mathcal{R}el$ be the following precategory:

•

Its objects are sets.
•

$\hom_{\mathcal{R}el}(X,Y)=X\to Y\to\mathsf{Prop}$ .
•

For a set $X$ , we have $1_{X}(x,x^{\prime}):\!\!\equiv(x=x^{\prime})$ .
•

For $R:\hom_{\mathcal{R}el}(X,Y)$ and $S:\hom_{\mathcal{R}el}(Y,Z)$ , their composite is defined by

$(S\circ R)(x,z):\!\!\equiv\Bigl{\|}\mathchoice{\sum_{y:Y}\,}{\mathchoice{{% \textstyle\sum_{(y:Y)}}}{\sum_{(y:Y)}}{\sum_{(y:Y)}}{\sum_{(y:Y)}}}{% \mathchoice{{\textstyle\sum_{(y:Y)}}}{\sum_{(y:Y)}}{\sum_{(y:Y)}}{\sum_{(y:Y)}% }}{\mathchoice{{\textstyle\sum_{(y:Y)}}}{\sum_{(y:Y)}}{\sum_{(y:Y)}}{\sum_{(y:% Y)}}}R(x,y)\times S(y,z)\Bigr{\|}.$

Suppose $R:\hom_{\mathcal{R}el}(X,Y)$ is an isomorphism, with inverse $S$ . We observe the following.

1.

If $R(x,y)$ and $S(y^{\prime},x)$ , then $(R\circ S)(y^{\prime},y)$ , and hence $y^{\prime}=y$ . Similarly, if $R(x,y)$ and $S(y,x^{\prime})$ , then $x=x^{\prime}$ .
2.

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

Suppose $R(x,y)$ . By 2, there merely exists a $y^{\prime}$ with $R(x,y^{\prime})$ and $S(y^{\prime},x)$ . But then by 1, merely $y^{\prime}=y$ , and hence $y^{\prime}=y$ since $Y$ is a set. Therefore, by transporting $S(y^{\prime},x)$ along this equality, we have $S(y,x)$ . In conclusion, $R(x,y)\to S(y,x)$ . Similarly, $S(y,x)\to R(x,y)$ .
4.

If $R(x,y)$ and $R(x,y^{\prime})$ , then by 3, $S(y^{\prime},x)$ , so that by 1, $y=y^{\prime}$ . 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:\hom_{\mathcal{R}el}(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:X\to Y$ sending each $x$ to this $y$ , which is an equivalence; hence $X=Y$ . With a little more work, we conclude that $\mathcal{R}el$ 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
\metatable