# 9.4 Equivalences

It is usual in category theory     to define an equivalence of categories to be a functor  $F:A\to B$ such that there exists a functor $G:B\to A$ and natural isomorphisms $FG\cong 1_{B}$ and $GF\cong 1_{A}$. Unlike the property of being an adjunction, however, this would not be a mere proposition without truncating it, for the same reasons that the type of quasi-inverses is ill-behaved (see \autorefsec:quasi-inverses). And as in \autorefsec:hae, we can avoid this by using the usual notion of adjoint equivalence.

By \autorefct:adjprop,\autorefct:isoprop, if $A$ is a category, then the type “$F$ is an equivalence of precategories” is a mere proposition.

###### Lemma 9.4.2.

If for $F:A\to B$ there exists $G:B\to A$ and isomorphisms $GF\cong 1_{A}$ and $FG\cong 1_{B}$, then $F$ is an equivalence of precategories.

###### Proof.

Just like the proof of \autorefthm:equiv-iso-adj for equivalences of types. ∎

###### Definition 9.4.3.

We say a functor $F:A\to B$ is if for all $a,b:A$, the function

 $F_{a,b}:\hom_{A}(a,b)\to\hom_{B}(Fa,Fb)$

is injective  , and full if for all $a,b:A$ this function is surjective  . If it is both (hence each $F_{a,b}$ is an equivalence) we say $F$ is fully faithful.

###### Definition 9.4.4.

We say a functor $F:A\to B$ is if for all $b:B$ there exists an $a:A$ such that $Fa\cong b$.

###### Lemma 9.4.5.

For any precategories $A$ and $B$ and functor $F:A\to B$, the following types are equivalent     .

1. 1.

$F$ is an equivalence of precategories.

2. 2.

$F$ is fully faithful and split essentially surjective.

###### Proof.

Suppose $F$ is an equivalence of precategories, with $G,\eta,\epsilon$ specified. Then we have the function

 $\displaystyle\hom_{B}(Fa,Fb)$ $\displaystyle\to\hom_{A}(a,b),$ $\displaystyle g$ $\displaystyle\mapsto{\eta_{b}}^{-1}\circ G(g)\circ\eta_{a}.$

For $f:\hom_{A}(a,b)$, we have

 ${\eta_{b}}^{-1}\circ G(F(f))\circ\eta_{a}={\eta_{b}}^{-1}\circ\eta_{b}\circ f=f$

while for $g:\hom_{B}(Fa,Fb)$ we have

 $\displaystyle F({\eta_{b}}^{-1}\circ G(g)\circ\eta_{a})$ $\displaystyle=F({\eta_{b}}^{-1})\circ F(G(g))\circ F(\eta_{a})$ $\displaystyle=\epsilon_{Fb}\circ F(G(g))\circ F(\eta_{a})$ $\displaystyle=g\circ\epsilon_{Fa}\circ F(\eta_{a})$ $\displaystyle=g$

using naturality of $\epsilon$, and the triangle identities twice. Thus, $F_{a,b}$ is an equivalence, so $F$ is fully faithful. Finally, for any $b:B$, we have $Gb:A$ and $\epsilon_{b}:FGb\cong b$.

On the other hand, suppose $F$ is fully faithful and split essentially surjective. Define $G_{0}:B_{0}\to A_{0}$ by sending $b:B$ to the $a:A$ given by the specified essential splitting, and write $\epsilon_{b}$ for the likewise specified isomorphism $FGb\cong b$.

Now for any $g:\hom_{B}(b,b^{\prime})$, define $G(g):\hom_{A}(Gb,Gb^{\prime})$ to be the unique morphism such that $F(G(g))={(\epsilon_{b^{\prime}})}^{-1}\circ g\circ\epsilon_{b}$ (which exists since $F$ is fully faithful). Finally, for $a:A$ define $\eta_{a}:\hom_{A}(a,GFa)$ to be the unique morphism such that $F\eta_{a}={\epsilon_{Fa}}^{-1}$. It is easy to verify that $G$ is a functor and that $(G,\eta,\epsilon)$ exhibit $F$ as an equivalence of precategories.

Now consider the composite 1$\to$2$\to$1. We clearly recover the same function $G_{0}:B_{0}\to A_{0}$. For the action of $G$ on hom-sets, we must show that for $g:\hom_{B}(b,b^{\prime})$, $G(g)$ is the (necessarily unique) morphism such that $F(G(g))={(\epsilon_{b^{\prime}})}^{-1}\circ g\circ\epsilon_{b}$. But this equation holds by the assumed naturality of $\epsilon$. We also clearly recover $\epsilon$, while $\eta$ is uniquely characterized by $F\eta_{a}={\epsilon_{Fa}}^{-1}$ (which is one of the triangle identities assumed to hold in the structure  of an equivalence of precategories). Thus, this composite is equal to the identity  .

Finally, consider the other composite 2$\to$1$\to$2. Since being fully faithful is a mere proposition, it suffices to observe that we recover, for each $b:B$, the same $a:A$ and isomorphism $Fa\cong b$. But this is clear, since we used this function and isomorphism to define $G_{0}$ and $\epsilon$ in 1, which in turn are precisely what we used to recover 2 again. Thus, the composites in both directions are equal to identities, hence we have an equivalence $\text{\ref{item:ct:ffeso1}}\simeq\text{\ref{item:ct:ffeso2}}$. ∎

However, if $B$ is not a category, then neither type in \autorefct:ffeso may necessarily be a mere proposition. This suggests considering as well the following notions.

###### Definition 9.4.6.

A functor $F:A\to B$ is essentially surjective if for all $b:B$, there merely exists an $a:A$ such that $Fa\cong b$. We say $F$ is a if it is fully faithful and essentially surjective.

###### Lemma 9.4.7.

If $F:A\to B$ is fully faithful and $A$ is a category, then for any $b:B$ the type $\mathchoice{\sum_{a:A}\,}{\mathchoice{{\textstyle\sum_{(a:A)}}}{\sum_{(a:A)}}{% \sum_{(a:A)}}{\sum_{(a:A)}}}{\mathchoice{{\textstyle\sum_{(a:A)}}}{\sum_{(a:A)% }}{\sum_{(a:A)}}{\sum_{(a:A)}}}{\mathchoice{{\textstyle\sum_{(a:A)}}}{\sum_{(a% :A)}}{\sum_{(a:A)}}{\sum_{(a:A)}}}(Fa\cong b)$ is a mere proposition. Hence a functor between categories is an equivalence if and only if it is a weak equivalence.

###### Proof.

Suppose given $(a,f)$ and $(a^{\prime},f^{\prime})$ in $\mathchoice{\sum_{a:A}\,}{\mathchoice{{\textstyle\sum_{(a:A)}}}{\sum_{(a:A)}}{% \sum_{(a:A)}}{\sum_{(a:A)}}}{\mathchoice{{\textstyle\sum_{(a:A)}}}{\sum_{(a:A)% }}{\sum_{(a:A)}}{\sum_{(a:A)}}}{\mathchoice{{\textstyle\sum_{(a:A)}}}{\sum_{(a% :A)}}{\sum_{(a:A)}}{\sum_{(a:A)}}}(Fa\cong b)$. Then ${f^{\prime}}^{-1}\circ f$ is an isomorphism $Fa\cong Fa^{\prime}$. Since $F$ is fully faithful, we have $g:a\cong a^{\prime}$ with $Fg={f^{\prime}}^{-1}\circ f$. And since $A$ is a category, we have $p:a=a^{\prime}$ with $\mathsf{idtoiso}(p)=g$. Now $Fg={f^{\prime}}^{-1}\circ f$ implies ${({(F_{0})}\mathopen{}\left({p}\right)\mathclose{})}_{*}\mathopen{}\left({f}% \right)\mathclose{}=f^{\prime}$, hence (by the characterization  of equalities in dependent pair types) $(a,f)=(a^{\prime},f^{\prime})$.

Thus, for fully faithful functors  whose domain is a category, essential surjectivity is equivalent to split essential surjectivity, and so being a weak equivalence is equivalent to being an equivalence. ∎

This is an important advantage of our category theory over set-based approaches. With a purely set-based definition of category, the statement “every fully faithful and essentially surjective functor is an equivalence of categories” is equivalent to the axiom of choice  $\mathsf{AC}$. Here we have it for free, as a category-theoretic version of the principle of unique choice (\autorefsec:unique-choice). (In fact, this property characterizes categories among precategories; see \autorefsec:rezk.)

On the other hand, the following characterization of equivalences of categories is perhaps even more useful.

###### Definition 9.4.8.

A functor $F:A\to B$ is an isomorphism of (pre)categories if $F$ is fully faithful and $F_{0}:A_{0}\to B_{0}$ is an equivalence of types.

This definition is an exception to our general rule (see \autorefsec:basics-equivalences) of only using the word “isomorphism” for sets and set-like objects. However, it does carry an appropriate connotation here, because for general precategories, isomorphism is stronger than equivalence.

Note that being an isomorphism of precategories is always a mere property. Let $A\cong B$ denote the type of isomorphisms of (pre)categories from $A$ to $B$.

###### Lemma 9.4.9.

For precategories $A$ and $B$ and $F:A\to B$, the following are equivalent.

1. 1.

$F$ is an isomorphism of precategories.

2. 2.

There exist $G:B\to A$ and $\eta:1_{A}=GF$ and $\epsilon:FG=1_{B}$ such that

 $\mathsf{ap}_{({\lambda}H.\,FH)}({\eta})=\mathsf{ap}_{({\lambda}K.\,KF)}({% \mathord{{\epsilon}^{-1}}}).$ (9.4.9)
3. 3.

There merely exist $G:B\to A$ and $\eta:1_{A}=GF$ and $\epsilon:FG=1_{B}$.

Note that if $B_{0}$ is not a 1-type, then (9.4.9) may not be a mere proposition.

###### Proof.

First note that since hom-sets are sets, equalities between equalities of functors are uniquely determined by their object-parts. Thus, by function extensionality, (9.4.9) is equivalent to

 ${(F_{0})}\mathopen{}\left({\eta_{0}}\right)\mathclose{}_{a}=\mathord{{(% \epsilon_{0})}^{-1}}_{F_{0}a}.$ (9.4.11)

for all $a:A_{0}$. Note that this is precisely the triangle identity for $G_{0}$, $\eta_{0}$, and $\epsilon_{0}$ to be a proof that $F_{0}$ is a half adjoint equivalence of types.

Now suppose 1. Let $G_{0}:B_{0}\to A_{0}$ be the inverse     of $F_{0}$, with $\eta_{0}:\mathsf{id}_{A_{0}}=G_{0}F_{0}$ and $\epsilon_{0}:F_{0}G_{0}=\mathsf{id}_{B_{0}}$ satisfying the triangle identity, which is precisely (9.4.11). Now define $G_{b,b^{\prime}}:\hom_{B}(b,b^{\prime})\to\hom_{A}(G_{0}b,G_{0}b^{\prime})$ by

 $G_{b,b^{\prime}}(g):\!\!\equiv{(F_{G_{0}b,G_{0}b^{\prime}})}^{-1}\Big{(}% \mathsf{idtoiso}(\mathord{{(\epsilon_{0})}^{-1}}_{b^{\prime}})\circ g\circ% \mathsf{idtoiso}((\epsilon_{0})_{b})\Big{)}$

(using the assumption  that $F$ is fully faithful). Since $\mathsf{idtoiso}$ takes inverses to inverses and concatenation to composition, and $F$ is a functor, it follows that $G$ is a functor.

By definition, we have $(GF)_{0}\equiv G_{0}F_{0}$, which is equal to $\mathsf{id}_{A_{0}}$ by $\eta_{0}$. To obtain $1_{A}=GF$, we need to show that when transported along $\eta_{0}$, the identity function of $\hom_{A}(a,a^{\prime})$ becomes equal to the composite $G_{Fa,Fa^{\prime}}\circ F_{a,a^{\prime}}$. In other words, for any $f:\hom_{A}(a,a^{\prime})$ we must have

 $\displaystyle\mathsf{idtoiso}((\eta_{0})_{a^{\prime}})\circ f\circ\mathsf{% idtoiso}(\mathord{{(\eta_{0})}^{-1}}_{a})\\ \displaystyle={(F_{GFa,GFa^{\prime}})}^{-1}\Big{(}\mathsf{idtoiso}(\mathord{{(% \epsilon_{0})}^{-1}}_{Fa^{\prime}})\circ F_{a,a^{\prime}}(f)\circ\mathsf{% idtoiso}((\epsilon_{0})_{Fa})\Big{)}.$

But this is equivalent to

 $\displaystyle(F_{GFa,GFa^{\prime}})\Big{(}\mathsf{idtoiso}((\eta_{0})_{a^{% \prime}})\circ f\circ\mathsf{idtoiso}(\mathord{{(\eta_{0})}^{-1}}_{a})\Big{)}% \\ \displaystyle=\mathsf{idtoiso}(\mathord{{(\epsilon_{0})}^{-1}}_{Fa^{\prime}})% \circ F_{a,a^{\prime}}(f)\circ\mathsf{idtoiso}((\epsilon_{0})_{Fa}).$

which follows from functoriality of $F$, the fact that $F$ preserves $\mathsf{idtoiso}$, and (9.4.11). Thus we have $\eta:1_{A}=GF$.

On the other side, we have $(FG)_{0}\equiv F_{0}G_{0}$, which is equal to $\mathsf{id}_{B_{0}}$ by $\epsilon_{0}$. To obtain $FG=1_{B}$, we need to show that when transported along $\epsilon_{0}$, the identity function of $\hom_{B}(b,b^{\prime})$ becomes equal to the composite $F_{Gb,Gb^{\prime}}\circ G_{b,b^{\prime}}$. That is, for any $g:\hom_{B}(b,b^{\prime})$ we must have

 $\displaystyle F_{Gb,Gb^{\prime}}\Big{(}{(F_{Gb,Gb^{\prime}})}^{-1}\Big{(}% \mathsf{idtoiso}(\mathord{{(\epsilon_{0})}^{-1}}_{b^{\prime}})\circ g\circ% \mathsf{idtoiso}((\epsilon_{0})_{b})\Big{)}\Big{)}\\ \displaystyle=\mathsf{idtoiso}((\mathord{{\epsilon_{0}}^{-1}})_{b^{\prime}})% \circ g\circ\mathsf{idtoiso}((\epsilon_{0})_{b}).$

But this is just the fact that ${(F_{Gb,Gb^{\prime}})}^{-1}$ is the inverse of $F_{Gb,Gb^{\prime}}$. And we have remarked that (9.4.9) is equivalent to (9.4.11), so 2 holds.

Conversely, suppose given 2; then the object-parts of $G$, $\eta$, and $\epsilon$ together with (9.4.11) show that $F_{0}$ is an equivalence of types. And for $a,a^{\prime}:A_{0}$, we define $\overline{G}_{a,a^{\prime}}:\hom_{B}(Fa,Fa^{\prime})\to\hom_{A}(a,a^{\prime})$ by

 $\overline{G}_{a,a^{\prime}}(g):\!\!\equiv\mathsf{idtoiso}(\mathord{{\eta}^{-1}% })_{a^{\prime}}\circ G(g)\circ\mathsf{idtoiso}(\eta)_{a}.$ (9.4.12)

By naturality of $\mathsf{idtoiso}(\eta)$, for any $f:\hom_{A}(a,a^{\prime})$ we have

 $\displaystyle\overline{G}_{a,a^{\prime}}(F_{a,a^{\prime}}(f))$ $\displaystyle=\mathsf{idtoiso}(\mathord{{\eta}^{-1}})_{a^{\prime}}\circ G(F(f)% )\circ\mathsf{idtoiso}(\eta)_{a}$ $\displaystyle=\mathsf{idtoiso}(\mathord{{\eta}^{-1}})_{a^{\prime}}\circ\mathsf% {idtoiso}(\eta)_{a^{\prime}}\circ f$ $\displaystyle=f.$

On the other hand, for $g:\hom_{B}(Fa,Fa^{\prime})$ we have

 $\displaystyle F_{a,a^{\prime}}(\overline{G}_{a,a^{\prime}}(g))$ $\displaystyle=F(\mathsf{idtoiso}(\mathord{{\eta}^{-1}})_{a^{\prime}})\circ F(G% (g))\circ F(\mathsf{idtoiso}(\eta)_{a})$ $\displaystyle=\mathsf{idtoiso}(\epsilon)_{Fa^{\prime}}\circ F(G(g))\circ% \mathsf{idtoiso}(\mathord{{\epsilon}^{-1}})_{Fa}$ $\displaystyle=\mathsf{idtoiso}(\epsilon)_{Fa^{\prime}}\circ\mathsf{idtoiso}(% \mathord{{\epsilon}^{-1}})_{Fa^{\prime}}\circ g$ $\displaystyle=g.$

(There are lemmas needed here regarding the compatibility of $\mathsf{idtoiso}$ and whiskering, which we leave it to the reader to state and prove.) Thus, $F_{a,a^{\prime}}$ is an equivalence, so $F$ is fully faithful; i.e. 1 holds.

Now the composite 1$\to$2$\to$1 is equal to the identity since 1 is a mere proposition. On the other side, tracing through the above constructions we see that the composite 2$\to$1$\to$2 essentially preserves the object-parts $G_{0}$, $\eta_{0}$, $\epsilon_{0}$, and the object-part of (9.4.9). And in the latter three cases, the object-part is all there is, since hom-sets are sets.

Thus, it suffices to show that we recover the action of $G$ on hom-sets. In other words, we must show that if $g:\hom_{B}(b,b^{\prime})$, then

 $G_{b,b^{\prime}}(g)=\overline{G}_{G_{0}b,G_{0}b^{\prime}}\Big{(}\mathsf{% idtoiso}(\mathord{{(\epsilon_{0})}^{-1}}_{b^{\prime}})\circ g\circ\mathsf{% idtoiso}((\epsilon_{0})_{b})\Big{)}$

where $\overline{G}$ is defined by (9.4.12). However, this follows from functoriality of $G$ and the other triangle identity, which we have seen in \autorefcha:equivalences is equivalent to (9.4.11).

Now since 1 is a mere proposition, so is 2, so it suffices to show they are logically equivalent to 3. Of course, 2$\to$3, so let us assume 3. Since 1 is a mere proposition, we may assume given $G$, $\eta$, and $\epsilon$. Then $G_{0}$ along with $\eta$ and $\epsilon$ imply that $F_{0}$ is an equivalence. Moreover, we also have natural isomorphisms $\mathsf{idtoiso}(\eta):1_{A}\cong GF$ and $\mathsf{idtoiso}(\epsilon):FG\cong 1_{B}$, so by \autorefct:adjointification, $F$ is an equivalence of precategories, and in particular fully faithful. ∎

From \autorefct:isoprecat2 and $\mathsf{idtoiso}$ in functor categories  , we conclude immediately that any isomorphism of precategories is an equivalence. For precategories, the converse can fail.

###### Example 9.4.13.

Let $X$ be a type and $x_{0}:X$ an element, and let $X_{\mathrm{ch}}$ denote the chaotic or indiscrete precategory on $X$. By definition, we have $(X_{\mathrm{ch}})_{0}:\!\!\equiv X$, and $\hom_{X_{\mathrm{ch}}}(x,x^{\prime}):\!\!\equiv\mathbf{1}$ for all $x,x^{\prime}$. Then the unique functor $X_{\mathrm{ch}}\to\mathbf{1}$ is an equivalence of precategories, but not an isomorphism unless $X$ is contractible  .

This example also shows that a precategory can be equivalent to a category without itself being a category. Of course, if a precategory is isomorphic to a category, then it must itself be a category.

However, for categories, the two notions coincide.

###### Lemma 9.4.14.

For categories $A$ and $B$, a functor $F:A\to B$ is an equivalence of categories if and only if it is an isomorphism of categories.

###### Proof.

Since both are mere properties, it suffices to show they are logically equivalent. So first suppose $F$ is an equivalence of categories, with $(G,\eta,\epsilon)$ given. We have already seen that $F$ is fully faithful. By \autorefct:functor-cat, the natural isomorphisms $\eta$ and $\epsilon$ yield identities $1_{A}=GF$ and $FG=1_{B}$, hence in particular identities $\mathsf{id}_{A}=G_{0}\circ F_{0}$ and $F_{0}\circ G_{0}=\mathsf{id}_{B}$. Thus, $F_{0}$ is an equivalence of types.

Conversely, suppose $F$ is fully faithful and $F_{0}$ is an equivalence of types, with inverse $G_{0}$, say. Then for each $b:B$ we have $G_{0}b:A$ and an identity $FGb=b$, hence an isomorphism $FGb\cong b$. Thus, by \autorefct:ffeso, $F$ is an equivalence of categories. ∎

Of course, there is yet a third notion of sameness for (pre)categories: equality. However, the univalence axiom implies that it coincides with isomorphism.

###### Lemma 9.4.15.

If $A$ and $B$ are precategories, then the function

 $(A=B)\to(A\cong B)$

###### Proof.

As usual for dependent sum types, to give an element of $A=B$ is equivalent to giving

• an identity $P_{0}:A_{0}=B_{0}$,

• for each $a,b:A_{0}$, an identity

 $P_{a,b}:\hom_{A}(a,b)=\hom_{B}({P_{0}}_{*}\mathopen{}\left({a}\right)% \mathclose{},{P_{0}}_{*}\mathopen{}\left({b}\right)\mathclose{}),$
• identities ${(P_{a,a})}_{*}\mathopen{}\left({1_{a}}\right)\mathclose{}=1_{{P_{0}}_{*}% \mathopen{}\left({a}\right)\mathclose{}}$ and ${(P_{a,c})}_{*}\mathopen{}\left({gf}\right)\mathclose{}={(P_{b,c})}_{*}% \mathopen{}\left({g}\right)\mathclose{}\circ{(P_{a,b})}_{*}\mathopen{}\left({f% }\right)\mathclose{}.$

(Again, we use the fact that the identity types of hom-sets are mere propositions.) However, by univalence, this is equivalent to giving

• an equivalence of types $F_{0}:A_{0}\simeq B_{0}$,

• for each $a,b:A_{0}$, an equivalence of types

 $F_{a,b}:\hom_{A}(a,b)\simeq\hom_{B}(F_{0}(a),F_{0}(b)),$
• and identities $F_{a,a}(1_{a})=1_{F_{0}(a)}$ and $F_{a,c}(gf)=F_{b,c}(g)\circ F_{a,b}(f)$.

But this consists exactly of a functor $F:A\to B$ that is an isomorphism of categories. And by induction on identity, this equivalence $(A=B)\simeq(A\cong B)$ is equal to the one obtained by induction. ∎

Thus, for categories, equality also coincides with equivalence. We can interpret this as saying that categories, functors, and natural transformations form, not just a pre-2-category, but a 2-category.

###### Theorem 9.4.16.

If $A$ and $B$ are categories, then the function

 $(A=B)\to(A\simeq B)$

(defined by induction from the identity functor) is an equivalence of types.

###### Proof.

By \autorefct:cat-eq-iso,\autorefct:eqv-levelwise. ∎

As a consequence, the type of categories is a 2-type. For since $A\simeq B$ is a subtype of the type of functors from $A$ to $B$, which are the objects of a category, it is a 1-type; hence the identity types $A=B$ are also 1-types.

Title 9.4 Equivalences
\metatable