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.

Definition 9.4.1.

A functor $F:A\to B$ is an equivalence of (pre)categories if it is a left adjoint for which $\eta$ and $\epsilon$ are isomorphisms. We write $A\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: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.

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: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)$

(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}:\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