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 quasiinverses is illbehaved (see \autorefsec:quasiinverses). And as in \autorefsec:hae, we can avoid this by using the usual notion of adjoint equivalence.
Definition 9.4.1.
A functor $F\mathrm{:}A\mathrm{\to}B$ is an equivalence of (pre)categories^{} if it is a left adjoint for which $\eta $ and $\u03f5$ are isomorphisms^{}. We write $A\mathrm{\simeq}B$ for the type of equivalences of categories from $A$ to $B$.
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\mathrm{:}A\mathrm{\to}B$ there exists $G\mathrm{:}B\mathrm{\to}A$ and isomorphisms $G\mathit{}F\mathrm{\cong}{\mathrm{1}}_{A}$ and $F\mathit{}G\mathrm{\cong}{\mathrm{1}}_{B}$, then $F$ is an equivalence of precategories.
Proof.
Just like the proof of \autorefthm:equivisoadj for equivalences of types. ∎
Definition 9.4.3.
We say a functor $F\mathrm{:}A\mathrm{\to}B$ is faithful^{} if for all $a\mathrm{,}b\mathrm{:}A$, the function
$${F}_{a,b}:{\mathrm{hom}}_{A}(a,b)\to {\mathrm{hom}}_{B}(Fa,Fb)$$ 
is injective^{}, and full if for all $a\mathrm{,}b\mathrm{:}A$ this function is surjective^{}. If it is both (hence each ${F}_{a\mathrm{,}b}$ is an equivalence) we say $F$ is fully faithful.
Definition 9.4.4.
We say a functor $F\mathrm{:}A\mathrm{\to}B$ is split essentially surjective if for all $b\mathrm{:}B$ there exists an $a\mathrm{:}A$ such that $F\mathit{}a\mathrm{\cong}b$.
Lemma 9.4.5.
For any precategories $A$ and $B$ and functor $F\mathrm{:}A\mathrm{\to}B$, the following types are equivalent^{}.

1.
$F$ is an equivalence of precategories.

2.
$F$ is fully faithful and split essentially surjective.
Proof.
Suppose $F$ is an equivalence of precategories, with $G,\eta ,\u03f5$ specified. Then we have the function
${\mathrm{hom}}_{B}(Fa,Fb)$  $\to {\mathrm{hom}}_{A}(a,b),$  
$g$  $\mapsto \eta _{b}{}^{1}\circ G(g)\circ {\eta}_{a}.$ 
For $f:{\mathrm{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:{\mathrm{hom}}_{B}(Fa,Fb)$ we have
$F(\eta _{b}{}^{1}\circ G(g)\circ {\eta}_{a})$  $=F(\eta _{b}{}^{1})\circ F(G(g))\circ F({\eta}_{a})$  
$={\u03f5}_{Fb}\circ F(G(g))\circ F({\eta}_{a})$  
$=g\circ {\u03f5}_{Fa}\circ F({\eta}_{a})$  
$=g$ 
using naturality of $\u03f5$, 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 ${\u03f5}_{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 ${\u03f5}_{b}$ for the likewise specified isomorphism $FGb\cong b$.
Now for any $g:{\mathrm{hom}}_{B}(b,{b}^{\prime})$, define $G(g):{\mathrm{hom}}_{A}(Gb,G{b}^{\prime})$ to be the unique morphism such that $F(G(g))={({\u03f5}_{{b}^{\prime}})}^{1}\circ g\circ {\u03f5}_{b}$ (which exists since $F$ is fully faithful). Finally, for $a:A$ define ${\eta}_{a}:{\mathrm{hom}}_{A}(a,GFa)$ to be the unique morphism such that $F{\eta}_{a}=\u03f5_{Fa}{}^{1}$. It is easy to verify that $G$ is a functor and that $(G,\eta ,\u03f5)$ 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 homsets, we must show that for $g:{\mathrm{hom}}_{B}(b,{b}^{\prime})$, $G(g)$ is the (necessarily unique) morphism such that $F(G(g))={({\u03f5}_{{b}^{\prime}})}^{1}\circ g\circ {\u03f5}_{b}$. But this equation holds by the assumed naturality of $\u03f5$. We also clearly recover $\u03f5$, while $\eta $ is uniquely characterized by $F{\eta}_{a}=\u03f5_{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 $\u03f5$ 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{1}\simeq \text{2}$. ∎
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\mathrm{:}A\mathrm{\to}B$ is essentially surjective if for all $b\mathrm{:}B$, there merely exists an $a\mathrm{:}A$ such that $F\mathit{}a\mathrm{\cong}b$. We say $F$ is a weak equivalence^{} if it is fully faithful and essentially surjective.
Being a weak equivalence is always a mere proposition. For categories, however, there is no difference^{} between equivalences and weak ones.
Lemma 9.4.7.
If $F\mathrm{:}A\mathrm{\to}B$ is fully faithful and $A$ is a category, then for any $b\mathrm{:}B$ the type ${\mathrm{\sum}}_{\mathrm{(}a\mathrm{:}A\mathrm{)}}\mathrm{(}Fa\mathrm{\cong}b\mathrm{)}$ 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 ${\sum}_{(a:A)}(Fa\cong b)$. Then $f^{\prime}{}^{1}\circ f$ is an isomorphism $Fa\cong F{a}^{\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 $\mathrm{\U0001d5c2\U0001d5bd\U0001d5cd\U0001d5c8\U0001d5c2\U0001d5cc\U0001d5c8}(p)=g$. Now $Fg=f^{\prime}{}^{1}\circ f$ implies ${(({F}_{0})\left(p\right))}_{*}\left(f\right)={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 setbased approaches. With a purely setbased definition of category, the statement “every fully faithful and essentially surjective functor is an equivalence of categories” is equivalent to the axiom of choice^{} $\mathrm{\U0001d5a0\U0001d5a2}$. Here we have it for free, as a categorytheoretic version of the principle of unique choice (\autorefsec:uniquechoice). (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\mathrm{:}A\mathrm{\to}B$ is an isomorphism of (pre)categories if $F$ is fully faithful and ${F}_{\mathrm{0}}\mathrm{:}{A}_{\mathrm{0}}\mathrm{\to}{B}_{\mathrm{0}}$ is an equivalence of types.
This definition is an exception to our general rule (see \autorefsec:basicsequivalences) of only using the word “isomorphism” for sets and setlike 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\mathrm{:}A\mathrm{\to}B$, the following are equivalent.

1.
$F$ is an isomorphism of precategories.

2.
There exist $G:B\to A$ and $\eta :{1}_{A}=GF$ and $\u03f5:FG={1}_{B}$ such that
$${\mathrm{\U0001d5ba\U0001d5c9}}_{(\lambda H.FH)}(\eta )={\mathrm{\U0001d5ba\U0001d5c9}}_{(\lambda K.KF)}({\u03f5}^{1}).$$ (9.4.9) 
3.
There merely exist $G:B\to A$ and $\eta :{1}_{A}=GF$ and $\u03f5:FG={1}_{B}$.
Note that if ${B}_{0}$ is not a 1type, then (9.4.9) may not be a mere proposition.
Proof.
First note that since homsets are sets, equalities between equalities of functors are uniquely determined by their objectparts. Thus, by function extensionality, (9.4.9) is equivalent to
$$({F}_{0}){\left({\eta}_{0}\right)}_{a}=({\u03f5}_{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 ${\u03f5}_{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}:{\mathrm{\U0001d5c2\U0001d5bd}}_{{A}_{0}}={G}_{0}{F}_{0}$ and ${\u03f5}_{0}:{F}_{0}{G}_{0}={\mathrm{\U0001d5c2\U0001d5bd}}_{{B}_{0}}$ satisfying the triangle identity, which is precisely (9.4.11). Now define ${G}_{b,{b}^{\prime}}:{\mathrm{hom}}_{B}(b,{b}^{\prime})\to {\mathrm{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}(\mathrm{\U0001d5c2\U0001d5bd\U0001d5cd\U0001d5c8\U0001d5c2\U0001d5cc\U0001d5c8}(({\u03f5}_{0})^{1}{}_{{b}^{\prime}})\circ g\circ \mathrm{\U0001d5c2\U0001d5bd\U0001d5cd\U0001d5c8\U0001d5c2\U0001d5cc\U0001d5c8}({({\u03f5}_{0})}_{b}))$$ 
(using the assumption^{} that $F$ is fully faithful). Since $\mathrm{\U0001d5c2\U0001d5bd\U0001d5cd\U0001d5c8\U0001d5c2\U0001d5cc\U0001d5c8}$ 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 ${\mathrm{\U0001d5c2\U0001d5bd}}_{{A}_{0}}$ by ${\eta}_{0}$. To obtain ${1}_{A}=GF$, we need to show that when transported along ${\eta}_{0}$, the identity function of ${\mathrm{hom}}_{A}(a,{a}^{\prime})$ becomes equal to the composite ${G}_{Fa,F{a}^{\prime}}\circ {F}_{a,{a}^{\prime}}$. In other words, for any $f:{\mathrm{hom}}_{A}(a,{a}^{\prime})$ we must have
$$\begin{array}{c}\mathrm{\U0001d5c2\U0001d5bd\U0001d5cd\U0001d5c8\U0001d5c2\U0001d5cc\U0001d5c8}({({\eta}_{0})}_{{a}^{\prime}})\circ f\circ \mathrm{\U0001d5c2\U0001d5bd\U0001d5cd\U0001d5c8\U0001d5c2\U0001d5cc\U0001d5c8}(({\eta}_{0})^{1}{}_{a})\hfill \\ \hfill ={({F}_{GFa,GF{a}^{\prime}})}^{1}\left(\mathrm{\U0001d5c2\U0001d5bd\U0001d5cd\U0001d5c8\U0001d5c2\U0001d5cc\U0001d5c8}(({\u03f5}_{0})^{1}{}_{F{a}^{\prime}})\circ {F}_{a,{a}^{\prime}}(f)\circ \mathrm{\U0001d5c2\U0001d5bd\U0001d5cd\U0001d5c8\U0001d5c2\U0001d5cc\U0001d5c8}({({\u03f5}_{0})}_{Fa})\right).\end{array}$$ 
But this is equivalent to
$$\begin{array}{c}({F}_{GFa,GF{a}^{\prime}})\left(\mathrm{\U0001d5c2\U0001d5bd\U0001d5cd\U0001d5c8\U0001d5c2\U0001d5cc\U0001d5c8}({({\eta}_{0})}_{{a}^{\prime}})\circ f\circ \mathrm{\U0001d5c2\U0001d5bd\U0001d5cd\U0001d5c8\U0001d5c2\U0001d5cc\U0001d5c8}(({\eta}_{0})^{1}{}_{a})\right)\hfill \\ \hfill =\mathrm{\U0001d5c2\U0001d5bd\U0001d5cd\U0001d5c8\U0001d5c2\U0001d5cc\U0001d5c8}(({\u03f5}_{0})^{1}{}_{F{a}^{\prime}})\circ {F}_{a,{a}^{\prime}}(f)\circ \mathrm{\U0001d5c2\U0001d5bd\U0001d5cd\U0001d5c8\U0001d5c2\U0001d5cc\U0001d5c8}({({\u03f5}_{0})}_{Fa}).\end{array}$$ 
which follows from functoriality of $F$, the fact that $F$ preserves $\mathrm{\U0001d5c2\U0001d5bd\U0001d5cd\U0001d5c8\U0001d5c2\U0001d5cc\U0001d5c8}$, 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 ${\mathrm{\U0001d5c2\U0001d5bd}}_{{B}_{0}}$ by ${\u03f5}_{0}$. To obtain $FG={1}_{B}$, we need to show that when transported along ${\u03f5}_{0}$, the identity function of ${\mathrm{hom}}_{B}(b,{b}^{\prime})$ becomes equal to the composite ${F}_{Gb,G{b}^{\prime}}\circ {G}_{b,{b}^{\prime}}$. That is, for any $g:{\mathrm{hom}}_{B}(b,{b}^{\prime})$ we must have
$$\begin{array}{c}{F}_{Gb,G{b}^{\prime}}\left({({F}_{Gb,G{b}^{\prime}})}^{1}\left(\mathrm{\U0001d5c2\U0001d5bd\U0001d5cd\U0001d5c8\U0001d5c2\U0001d5cc\U0001d5c8}(({\u03f5}_{0})^{1}{}_{{b}^{\prime}})\circ g\circ \mathrm{\U0001d5c2\U0001d5bd\U0001d5cd\U0001d5c8\U0001d5c2\U0001d5cc\U0001d5c8}({({\u03f5}_{0})}_{b})\right)\right)\hfill \\ \hfill =\mathrm{\U0001d5c2\U0001d5bd\U0001d5cd\U0001d5c8\U0001d5c2\U0001d5cc\U0001d5c8}({(\u03f5_{0}{}^{1})}_{{b}^{\prime}})\circ g\circ \mathrm{\U0001d5c2\U0001d5bd\U0001d5cd\U0001d5c8\U0001d5c2\U0001d5cc\U0001d5c8}({({\u03f5}_{0})}_{b}).\end{array}$$ 
But this is just the fact that ${({F}_{Gb,G{b}^{\prime}})}^{1}$ is the inverse of ${F}_{Gb,G{b}^{\prime}}$. And we have remarked that (9.4.9) is equivalent to (9.4.11), so 2 holds.
Conversely, suppose given 2; then the objectparts of $G$, $\eta $, and $\u03f5$ 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}}:{\mathrm{hom}}_{B}(Fa,F{a}^{\prime})\to {\mathrm{hom}}_{A}(a,{a}^{\prime})$ by
$${\overline{G}}_{a,{a}^{\prime}}(g):\equiv \mathrm{\U0001d5c2\U0001d5bd\U0001d5cd\U0001d5c8\U0001d5c2\U0001d5cc\U0001d5c8}{({\eta}^{1})}_{{a}^{\prime}}\circ G(g)\circ \mathrm{\U0001d5c2\U0001d5bd\U0001d5cd\U0001d5c8\U0001d5c2\U0001d5cc\U0001d5c8}{(\eta )}_{a}.$$  (9.4.12) 
By naturality of $\mathrm{\U0001d5c2\U0001d5bd\U0001d5cd\U0001d5c8\U0001d5c2\U0001d5cc\U0001d5c8}(\eta )$, for any $f:{\mathrm{hom}}_{A}(a,{a}^{\prime})$ we have
${\overline{G}}_{a,{a}^{\prime}}({F}_{a,{a}^{\prime}}(f))$  $=\mathrm{\U0001d5c2\U0001d5bd\U0001d5cd\U0001d5c8\U0001d5c2\U0001d5cc\U0001d5c8}{({\eta}^{1})}_{{a}^{\prime}}\circ G(F(f))\circ \mathrm{\U0001d5c2\U0001d5bd\U0001d5cd\U0001d5c8\U0001d5c2\U0001d5cc\U0001d5c8}{(\eta )}_{a}$  
$=\mathrm{\U0001d5c2\U0001d5bd\U0001d5cd\U0001d5c8\U0001d5c2\U0001d5cc\U0001d5c8}{({\eta}^{1})}_{{a}^{\prime}}\circ \mathrm{\U0001d5c2\U0001d5bd\U0001d5cd\U0001d5c8\U0001d5c2\U0001d5cc\U0001d5c8}{(\eta )}_{{a}^{\prime}}\circ f$  
$=f.$ 
On the other hand, for $g:{\mathrm{hom}}_{B}(Fa,F{a}^{\prime})$ we have
${F}_{a,{a}^{\prime}}({\overline{G}}_{a,{a}^{\prime}}(g))$  $=F(\mathrm{\U0001d5c2\U0001d5bd\U0001d5cd\U0001d5c8\U0001d5c2\U0001d5cc\U0001d5c8}{({\eta}^{1})}_{{a}^{\prime}})\circ F(G(g))\circ F(\mathrm{\U0001d5c2\U0001d5bd\U0001d5cd\U0001d5c8\U0001d5c2\U0001d5cc\U0001d5c8}{(\eta )}_{a})$  
$=\mathrm{\U0001d5c2\U0001d5bd\U0001d5cd\U0001d5c8\U0001d5c2\U0001d5cc\U0001d5c8}{(\u03f5)}_{F{a}^{\prime}}\circ F(G(g))\circ \mathrm{\U0001d5c2\U0001d5bd\U0001d5cd\U0001d5c8\U0001d5c2\U0001d5cc\U0001d5c8}{({\u03f5}^{1})}_{Fa}$  
$=\mathrm{\U0001d5c2\U0001d5bd\U0001d5cd\U0001d5c8\U0001d5c2\U0001d5cc\U0001d5c8}{(\u03f5)}_{F{a}^{\prime}}\circ \mathrm{\U0001d5c2\U0001d5bd\U0001d5cd\U0001d5c8\U0001d5c2\U0001d5cc\U0001d5c8}{({\u03f5}^{1})}_{F{a}^{\prime}}\circ g$  
$=g.$ 
(There are lemmas needed here regarding the compatibility of $\mathrm{\U0001d5c2\U0001d5bd\U0001d5cd\U0001d5c8\U0001d5c2\U0001d5cc\U0001d5c8}$ 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 objectparts ${G}_{0}$, ${\eta}_{0}$, ${\u03f5}_{0}$, and the objectpart of (9.4.9). And in the latter three cases, the objectpart is all there is, since homsets are sets.
Thus, it suffices to show that we recover the action of $G$ on homsets. In other words, we must show that if $g:{\mathrm{hom}}_{B}(b,{b}^{\prime})$, then
$${G}_{b,{b}^{\prime}}(g)={\overline{G}}_{{G}_{0}b,{G}_{0}{b}^{\prime}}\left(\mathrm{\U0001d5c2\U0001d5bd\U0001d5cd\U0001d5c8\U0001d5c2\U0001d5cc\U0001d5c8}(({\u03f5}_{0})^{1}{}_{{b}^{\prime}})\circ g\circ \mathrm{\U0001d5c2\U0001d5bd\U0001d5cd\U0001d5c8\U0001d5c2\U0001d5cc\U0001d5c8}({({\u03f5}_{0})}_{b})\right)$$ 
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 $\u03f5$. Then ${G}_{0}$ along with $\eta $ and $\u03f5$ imply that ${F}_{0}$ is an equivalence. Moreover, we also have natural isomorphisms $\mathrm{\U0001d5c2\U0001d5bd\U0001d5cd\U0001d5c8\U0001d5c2\U0001d5cc\U0001d5c8}(\eta ):{1}_{A}\cong GF$ and $\mathrm{\U0001d5c2\U0001d5bd\U0001d5cd\U0001d5c8\U0001d5c2\U0001d5cc\U0001d5c8}(\u03f5):FG\cong {1}_{B}$, so by \autorefct:adjointification, $F$ is an equivalence of precategories, and in particular fully faithful. ∎
From \autorefct:isoprecat2 and $\mathrm{\U0001d5c2\U0001d5bd\U0001d5cd\U0001d5c8\U0001d5c2\U0001d5cc\U0001d5c8}$ 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}_{\mathrm{0}}\mathrm{:}X$ an element, and let ${X}_{\mathrm{ch}}$ denote the chaotic or indiscrete precategory on $X$. By definition, we have ${\mathrm{(}{X}_{\mathrm{ch}}\mathrm{)}}_{\mathrm{0}}\mathrm{:}\mathrm{\equiv}X$, and ${\mathrm{hom}}_{{X}_{\mathrm{ch}}}\mathrm{(}x\mathrm{,}{x}^{\mathrm{\prime}}\mathrm{)}\mathrm{:}\mathrm{\equiv}\mathrm{1}$ for all $x\mathrm{,}{x}^{\mathrm{\prime}}$. Then the unique functor ${X}_{\mathrm{ch}}\mathrm{\to}\mathrm{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\mathrm{:}A\mathrm{\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 ,\u03f5)$ given. We have already seen that $F$ is fully faithful. By \autorefct:functorcat, the natural isomorphisms $\eta $ and $\u03f5$ yield identities ${1}_{A}=GF$ and $FG={1}_{B}$, hence in particular identities ${\mathrm{\U0001d5c2\U0001d5bd}}_{A}={G}_{0}\circ {F}_{0}$ and ${F}_{0}\circ {G}_{0}={\mathrm{\U0001d5c2\U0001d5bd}}_{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)$$ 
(defined by induction^{} from the identity functor) is an equivalence of types.
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}:{\mathrm{hom}}_{A}(a,b)={\mathrm{hom}}_{B}(P_{0}{}_{*}\left(a\right),P_{0}{}_{*}\left(b\right)),$$ 
•
identities ${({P}_{a,a})}_{*}\left({1}_{a}\right)={1}_{P_{0}{}_{*}\left(a\right)}$ and ${({P}_{a,c})}_{*}\left(gf\right)={({P}_{b,c})}_{*}\left(g\right)\circ {({P}_{a,b})}_{*}\left(f\right).$
(Again, we use the fact that the identity types of homsets 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}:{\mathrm{hom}}_{A}(a,b)\simeq {\mathrm{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 pre2category, but a 2category.
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:cateqiso,\autorefct:eqvlevelwise. ∎
As a consequence, the type of categories is a 2type. 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 1type; hence the identity types $A=B$ are also 1types.
Title  9.4 Equivalences 

\metatable 