We proceed by showing:
Let $F\colon \mathcal{C}\to \mathcal{D}$ be an equivalence with inverse $G\colon \mathcal{D}\to \mathcal{E}$, and write $GF\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}G\circ F$. We claim that $F$ is full, faithful, and essentially surjective:
-
•
Faithfulness: Let $f,g\in \operatorname {\mathrm{Hom}}_{\mathcal{C}}(A,B)$ with $F(f)=F(g)$. Then $GF(f)=GF(g)$ and we have the following diagrams:
Since $\eta ^{-1}$ is natural, these commute. We then have
\begin{align*} f\circ \eta ^{-1}_{A} & = \eta ^{-1}_{B}\circ GF(f)\\ & = \eta ^{-1}_{B}\circ GF(g)\\ & = g\circ \eta ^{-1}_{A}. \end{align*}
Precomposing both sides with $\eta _{A}$ then gives $f=g$, showing $F$ to be faithful.
-
•
Fullness: Given $f\in \operatorname {\mathrm{Hom}}_{\mathcal{D}}(F(A),F(B))$, define a morphism $h\colon A\to B$ by
\[ h\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\eta ^{-1}_{B}\circ G(f)\circ \eta _{A}, \]
yielding the commutative diagram
We must show $F(h) = f$. Since $(G,F,\epsilon ^{-1},\eta ^{-1})$ is also an equivalence due to Item 3, the functor $G$ is faithful, so it suffices to show $GF(h) = G(f)$.
From the naturality of $\eta $ applied to $\eta _{A}\colon A\to GF(A)$, we have
for all $A\in \operatorname {\mathrm{Obj}}(\mathcal{C})$. Since $\eta $ is an isomorphism, this implies $\eta _{GF(A)} = GF(\eta _{A})$.
By applying $GF$ to the diagram $(\dagger )$ and incorporating the equality, we see that the diagram
must commute. By naturality of $\eta $, so does the diagram We then have
\begin{align*} \eta _{GF(B)}\circ GF(h) & = GFG(f)\circ \eta _{GF(A)}\\ & = \eta _{GF(B)}\circ G(f). \end{align*}
Postcomposing with $\eta ^{-1}_{GF(B)}$ then gives $GF(h) = G(f)$. This shows $F$ to be full.
-
•
Essential surjectivity: Let $B\in \operatorname {\mathrm{Obj}}(\mathcal{D})$. We need to find some $A\in \operatorname {\mathrm{Obj}}(\mathcal{C})$ with $F(A)\cong B$. Choose $A\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}G(B)$. Then $\epsilon _{B}\colon FG(B)\to B$ is an isomorphism by assumption. Hence $F$ is essentially surjective.
Since $F$ is essentially surjective and $\mathcal{C}$ and $\mathcal{D}$ are small, we can choose, using the axiom of choice, for each $B\in \operatorname {\mathrm{Obj}}(\mathcal{D})$, an object $j_{B}$ of $\mathcal{C}$ and an isomorphism $i_{B}\colon B\overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }F(j_{B})$ of $\mathcal{D}$.
Since $F$ is fully faithful, we can extend the assignment $B\mapsto j_{B}$ to a unique functor $j\colon \mathcal{D}\to \mathcal{C}$ such that the isomorphisms $i_{B}\colon B\overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }F(j_{B})$ assemble into a natural isomorphism $\eta \colon \operatorname {\mathrm{id}}_{\mathcal{D}}\mathbin {\overset {\mathord {\sim }}{\Longrightarrow }}F\circ j$, with a similar natural isomorphism $\epsilon \colon \operatorname {\mathrm{id}}_{\mathcal{C}}\mathbin {\overset {\mathord {\sim }}{\Longrightarrow }}j\circ F$. Hence $F$ is an equivalence.
This follows from Item 4 of Proposition 11.1.3.1.3.
This follows from Item 4 of Proposition 11.1.3.1.3 and Item 5 of this proposition.
Omitted.
Item 2: Invariance Under Natural Isomorphism
Omitted.
The result follows from the fact that
\begin{align*} \epsilon ^{-1} & \colon \operatorname {\mathrm{id}}_{\mathcal{D}} \mathbin {\overset {\mathord {\sim }}{\Longrightarrow }}F \circ G,\\ \eta ^{-1} & \colon G\circ F \mathbin {\overset {\mathord {\sim }}{\Longrightarrow }}\operatorname {\mathrm{id}}_{\mathcal{C}} \end{align*}
are natural isomorphisms iff $\epsilon $ and $\eta $ are.
Let $F\colon \mathcal{C}\to \mathcal{D}$ and $G\colon \mathcal{D}\to \mathcal{E}$ be functors.
-
•
When $F$ and $G$ Are Equivalences: By Item 5, if $F$ and $G$ are equivalences, then so is $G\circ F$.
-
•
When $G$ and $G\circ F$ Are Equivalences: If $G\circ F$ and $G$ are equivalences, note that by Item 5 and Item 3, so are $G^{-1}$ and $G^{-1}\circ G\circ F\cong F$. Therefore $F$ will be an equivalence by Item 2.
-
•
When $F$ and $G\circ F$ Are Equivalences: If $G\circ F$ and $F$ are equivalences, so are $F^{-1}$ and $G\circ F\circ F^{-1}\cong G$ by Item 5 and Item 3. Therefore $G$ will be an equivalence by Item 2.
This finishes the proof.
Item 5: Stability Under Composition
Assume $(F,G,\eta ,\epsilon )$ and $(F',G',\eta ',\epsilon ')$ are equivalences as in the theorem statement. Define a natural transformation
\[ \eta ^{\circ }\colon \operatorname {\mathrm{id}}_{\mathcal{C}}\Longrightarrow (G\circ G')\circ (F'\circ F) \]
as the composition
and a natural transformation
\[ \epsilon ^{\circ } \colon (F'\circ F)\circ (G\circ G')\Longrightarrow \operatorname {\mathrm{id}}_{\mathcal{E}} \]
as the composition
In other words, define
\begin{align*} \eta ^{\circ } & = (\operatorname {\mathrm{id}}_{G}\mathbin {\star }\eta '\mathbin {\star }\operatorname {\mathrm{id}}_{F})\circ \eta ,\\ \epsilon ^{\circ } & = \epsilon ’\circ (\operatorname {\mathrm{id}}_{F'}\mathbin {\star }\epsilon \mathbin {\star }\operatorname {\mathrm{id}}_{G'}),\end{align*}
so that the components of $\eta ^{\circ }$ and $\epsilon ^{\circ }$ are of the form
\begin{align*} \eta ^{\circ }_{A} & = G(\eta '_{F(A)})\circ \eta _{A},\\ \epsilon ^{\circ }_{A} & = \epsilon ’_{A}\circ F’(\epsilon _{G'(A)}).\end{align*}
Since $\eta ^{\circ }$ and $\epsilon ^{\circ }$ are compositions of whiskerings of natural isomorphisms, they are natural transformations by Definition 11.9.5.1.2 and natural isomorphisms by Item 5b and Item 5c of Item 5 of Proposition 11.9.5.1.3.
Thus, $(F'\circ F,G\circ G',\eta ^{\circ },\epsilon ^{\circ })$ is an equivalence.
Item 6: Equivalences vs.
Adjoint Equivalences
See Proposition 4.4.5 of [Riehl, Category Theory in Context].
Item 7: Equivalences of Groupoids
See Proposition 4.4 of [nLab Authors, Groupoid].
