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 sec:quasi-inverses). And as in sec: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 $ϵ$ are isomorphisms. We write $A\mathrm{\simeq }B$ for the type of equivalences of categories from $A$ to $B$.

By ct:adjprop,ct: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 thm:equiv-iso-adj 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 ,ϵ$ 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)$

$={ϵ}_{Fb}\circ F(G(g))\circ F({\eta }_a)$

$=g\circ {ϵ}_{Fa}\circ F({\eta }_a)$

$=g$

using naturality of $ϵ$, 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 ${ϵ}_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 ${ϵ}_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))={({ϵ}_{b^{\prime }})}^{-1}\circ g\circ {ϵ}_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=ϵ_{Fa}{}^{-1}$. It is easy to verify that $G$ is a functor and that $(G,\eta ,ϵ)$ 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:{\mathrm{hom}}_B(b,b^{\prime })$, $G(g)$ is the (necessarily unique) morphism such that $F(G(g))={({ϵ}_{b^{\prime }})}^{-1}\circ g\circ {ϵ}_b$. But this equation holds by the assumed naturality of $ϵ$. We also clearly recover $ϵ$, while $\eta$ is uniquely characterized by $F{\eta }_a=ϵ_{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 $ϵ$ 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{<a href="\#I1.i1" title="1. ‣ Lemma 9.4.5. ‣ 9.4 Equivalences" class="ltx\_ref"><span class="ltx\_text ltx\_ref\_tag">1</span></a>}\simeq \text{<a href="\#I1.i2" title="2. ‣ Lemma 9.4.5. ‣ 9.4 Equivalences" class="ltx\_ref"><span class="ltx\_text ltx\_ref\_tag">2</span></a>}$. ∎

However, if $B$ is not a category, then neither type in ct: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{𝗂𝖽𝗍𝗈𝗂𝗌𝗈}(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 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 $\mathrm{𝖠𝖢}$. Here we have it for free, as a category-theoretic version of the principle of unique choice (sec:unique-choice). (In fact, this property characterizes categories among precategories; see sec: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 sec: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\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 $ϵ:FG=1_B$ such that

   $${\mathrm{𝖺𝗉}}_{(\lambda H.FH)}(\eta )={\mathrm{𝖺𝗉}}_{(\lambda K.KF)}({ϵ}^{-1}).$$ (9.4.9)

3. There merely exist $G:B\to A$ and $\eta :1_A=GF$ and $ϵ: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){\left({\eta }_0\right)}_a=({ϵ}_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 ${ϵ}_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{𝗂𝖽}}_{A_0}=G_0{F}_0$ and ${ϵ}_0:F_0{G}_0={\mathrm{𝗂𝖽}}_{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{𝗂𝖽𝗍𝗈𝗂𝗌𝗈}(({ϵ}_0)^{-1}{}_{b^{\prime }})\circ g\circ \mathrm{𝗂𝖽𝗍𝗈𝗂𝗌𝗈}({({ϵ}_0)}_b))$$

(using the assumption that $F$ is fully faithful). Since $\mathrm{𝗂𝖽𝗍𝗈𝗂𝗌𝗈}$ 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{𝗂𝖽}}_{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{𝗂𝖽𝗍𝗈𝗂𝗌𝗈}({({\eta }_0)}_{a^{\prime }})\circ f\circ \mathrm{𝗂𝖽𝗍𝗈𝗂𝗌𝗈}(({\eta }_0)^{-1}{}_a)\hfill \\ \hfill ={(F_{GFa,GF{a}^{\prime }})}^{-1}\left(\mathrm{𝗂𝖽𝗍𝗈𝗂𝗌𝗈}(({ϵ}_0)^{-1}{}_{F{a}^{\prime }})\circ F_{a,a^{\prime }}(f)\circ \mathrm{𝗂𝖽𝗍𝗈𝗂𝗌𝗈}({({ϵ}_0)}_{Fa})\right).\end{array}$$

But this is equivalent to

$$\begin{array}{c}(F_{GFa,GF{a}^{\prime }})\left(\mathrm{𝗂𝖽𝗍𝗈𝗂𝗌𝗈}({({\eta }_0)}_{a^{\prime }})\circ f\circ \mathrm{𝗂𝖽𝗍𝗈𝗂𝗌𝗈}(({\eta }_0)^{-1}{}_a)\right)\hfill \\ \hfill =\mathrm{𝗂𝖽𝗍𝗈𝗂𝗌𝗈}(({ϵ}_0)^{-1}{}_{F{a}^{\prime }})\circ F_{a,a^{\prime }}(f)\circ \mathrm{𝗂𝖽𝗍𝗈𝗂𝗌𝗈}({({ϵ}_0)}_{Fa}).\end{array}$$

which follows from functoriality of $F$, the fact that $F$ preserves $\mathrm{𝗂𝖽𝗍𝗈𝗂𝗌𝗈}$, 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{𝗂𝖽}}_{B_0}$ by ${ϵ}_0$. To obtain $FG=1_B$, we need to show that when transported along ${ϵ}_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{𝗂𝖽𝗍𝗈𝗂𝗌𝗈}(({ϵ}_0)^{-1}{}_{b^{\prime }})\circ g\circ \mathrm{𝗂𝖽𝗍𝗈𝗂𝗌𝗈}({({ϵ}_0)}_b)\right)\right)\hfill \\ \hfill =\mathrm{𝗂𝖽𝗍𝗈𝗂𝗌𝗈}({(ϵ_0{}^{-1})}_{b^{\prime }})\circ g\circ \mathrm{𝗂𝖽𝗍𝗈𝗂𝗌𝗈}({({ϵ}_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 object-parts of $G$, $\eta$, and $ϵ$ 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{𝗂𝖽𝗍𝗈𝗂𝗌𝗈}{({\eta }^{-1})}_{a^{\prime }}\circ G(g)\circ \mathrm{𝗂𝖽𝗍𝗈𝗂𝗌𝗈}{(\eta )}_a.$$ (9.4.12)

By naturality of $\mathrm{𝗂𝖽𝗍𝗈𝗂𝗌𝗈}(\eta )$, for any $f:{\mathrm{hom}}_A(a,a^{\prime })$ we have

${\overline{G}}_{a,a^{\prime }}(F_{a,a^{\prime }}(f))$ $=\mathrm{𝗂𝖽𝗍𝗈𝗂𝗌𝗈}{({\eta }^{-1})}_{a^{\prime }}\circ G(F(f))\circ \mathrm{𝗂𝖽𝗍𝗈𝗂𝗌𝗈}{(\eta )}_a$

$=\mathrm{𝗂𝖽𝗍𝗈𝗂𝗌𝗈}{({\eta }^{-1})}_{a^{\prime }}\circ \mathrm{𝗂𝖽𝗍𝗈𝗂𝗌𝗈}{(\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{𝗂𝖽𝗍𝗈𝗂𝗌𝗈}{({\eta }^{-1})}_{a^{\prime }})\circ F(G(g))\circ F(\mathrm{𝗂𝖽𝗍𝗈𝗂𝗌𝗈}{(\eta )}_a)$

$=\mathrm{𝗂𝖽𝗍𝗈𝗂𝗌𝗈}{(ϵ)}_{F{a}^{\prime }}\circ F(G(g))\circ \mathrm{𝗂𝖽𝗍𝗈𝗂𝗌𝗈}{({ϵ}^{-1})}_{Fa}$

$=\mathrm{𝗂𝖽𝗍𝗈𝗂𝗌𝗈}{(ϵ)}_{F{a}^{\prime }}\circ \mathrm{𝗂𝖽𝗍𝗈𝗂𝗌𝗈}{({ϵ}^{-1})}_{F{a}^{\prime }}\circ g$

$=g.$

(There are lemmas needed here regarding the compatibility of $\mathrm{𝗂𝖽𝗍𝗈𝗂𝗌𝗈}$ 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$, ${ϵ}_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:{\mathrm{hom}}_B(b,b^{\prime })$, then

$$G_{b,b^{\prime }}(g)={\overline{G}}_{G_{0}b,G_0{b}^{\prime }}\left(\mathrm{𝗂𝖽𝗍𝗈𝗂𝗌𝗈}(({ϵ}_0)^{-1}{}_{b^{\prime }})\circ g\circ \mathrm{𝗂𝖽𝗍𝗈𝗂𝗌𝗈}({({ϵ}_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 cha: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 $ϵ$. Then $G_0$ along with $\eta$ and $ϵ$ imply that $F_0$ is an equivalence. Moreover, we also have natural isomorphisms $\mathrm{𝗂𝖽𝗍𝗈𝗂𝗌𝗈}(\eta ):1_A\cong GF$ and $\mathrm{𝗂𝖽𝗍𝗈𝗂𝗌𝗈}(ϵ):FG\cong 1_B$, so by ct:adjointification, $F$ is an equivalence of precategories, and in particular fully faithful. ∎

From ct:isoprecat2 and $\mathrm{𝗂𝖽𝗍𝗈𝗂𝗌𝗈}$ 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 ,ϵ)$ given. We have already seen that $F$ is fully faithful. By ct:functor-cat, the natural isomorphisms $\eta$ and $ϵ$ yield identities $1_A=GF$ and $FG=1_B$, hence in particular identities ${\mathrm{𝗂𝖽}}_A=G_0\circ F_0$ and $F_0\circ G_0={\mathrm{𝗂𝖽}}_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 ct: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 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}:{\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 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 ct:cat-eq-iso,ct: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