[proofplan] An isomorphism of categories gives strict equalities $G\circ F=\operatorname{id}_{\mathcal C}$ and $F\circ G=\operatorname{id}_{\mathcal D}$. To prove that $F$ is an equivalence, we reinterpret these equalities as natural isomorphisms whose components are identity morphisms. The only point to check is naturality, which follows because the equalities of functors hold on both objects and morphisms. [/proofplan] [step:Build the unit natural isomorphism from the equality $G\circ F=\operatorname{id}_{\mathcal C}$] Define a natural transformation $\eta:\operatorname{id}_{\mathcal C}\Rightarrow G\circ F$ as follows. For each object $X$ of $\mathcal C$, the equality of functors $G\circ F=\operatorname{id}_{\mathcal C}$ gives \begin{align*} (G\circ F)(X)=X. \end{align*} Set \begin{align*} \eta_X:=\operatorname{id}_X:X\to (G\circ F)(X). \end{align*} This is an isomorphism in $\mathcal C$, with inverse $\operatorname{id}_X$. It remains to verify naturality. Let $f:X\to X'$ be a morphism in $\mathcal C$. Since $G\circ F=\operatorname{id}_{\mathcal C}$ as functors, we have \begin{align*} (G\circ F)(f)=f. \end{align*} Therefore \begin{align*} (G\circ F)(f)\circ \eta_X &= f\circ \operatorname{id}_X \\ &= f \\ &= \operatorname{id}_{X'}\circ f \\ &= \eta_{X'}\circ f. \end{align*} Thus $\eta:\operatorname{id}_{\mathcal C}\Rightarrow G\circ F$ is a natural isomorphism. [/step] [step:Build the counit natural isomorphism from the equality $F\circ G=\operatorname{id}_{\mathcal D}$] Define a natural transformation $\varepsilon:F\circ G\Rightarrow \operatorname{id}_{\mathcal D}$ as follows. For each object $Y$ of $\mathcal D$, the equality of functors $F\circ G=\operatorname{id}_{\mathcal D}$ gives \begin{align*} (F\circ G)(Y)=Y. \end{align*} Set \begin{align*} \varepsilon_Y:=\operatorname{id}_Y:(F\circ G)(Y)\to Y. \end{align*} This is an isomorphism in $\mathcal D$, with inverse $\operatorname{id}_Y$. Let $h:Y\to Y'$ be a morphism in $\mathcal D$. Since $F\circ G=\operatorname{id}_{\mathcal D}$ as functors, we have \begin{align*} (F\circ G)(h)=h. \end{align*} Hence \begin{align*} h\circ \varepsilon_Y &= h\circ \operatorname{id}_Y \\ &= h \\ &= \operatorname{id}_{Y'}\circ h \\ &= \varepsilon_{Y'}\circ (F\circ G)(h). \end{align*} Thus $\varepsilon:F\circ G\Rightarrow \operatorname{id}_{\mathcal D}$ is a natural isomorphism. [/step] [step:Conclude that $F$ is an equivalence of categories] The functor $G:\mathcal D\to\mathcal C$ together with the natural isomorphisms \begin{align*} \eta:\operatorname{id}_{\mathcal C}\Rightarrow G\circ F, \qquad \varepsilon:F\circ G\Rightarrow \operatorname{id}_{\mathcal D} \end{align*} is precisely the data of a quasi-inverse for $F$. Therefore $F:\mathcal C\to\mathcal D$ is an equivalence of categories. [/step]