A functor is an equivalence exactly when it is fully faithful and split essentially surjective, without Choice

Suppose first that $F$ has quasi-inverse $G$, unit $\eta:1_{\mathcal C}\Rightarrow GF$, and counit $\varepsilon:FG\Rightarrow1_{\mathcal D}$. Then $D\mapsto(GD,\varepsilon_D)$ explicitly splits essential surjectivity.

Conversely, assume $F$ is fully faithful and comes with objects $C_D$ and isomorphisms $\varepsilon_D:FC_D\to D$. Define $GD=C_D$, and for $u:D\to E$ define $G(u)$ as the unique morphism whose image under $F$ is $\varepsilon_E^{-1}u\varepsilon_D$; fullness gives existence and faithfulness gives uniqueness.

Naturality and invertibility of $\eta$ show faithfulness: if $Ff=Fg$, then $GFf=GFg$, so $\eta_B f=GFf\,\eta_A=GFg\,\eta_A=\eta_B g$ and $f=g$.

The defining equation makes $G(1_D)=1_{GD}$ and $G(vu)=G(v)G(u)$ after applying faithful $F$, so $G$ is a functor, and the same equation is precisely naturality of $\varepsilon:FG\Rightarrow1_{\mathcal D}$.

Put $\delta_A=\varepsilon_{FA}\circ F(\eta_A)$, an automorphism of $FA$. For $u:FA\to FB$, set $v=\delta_Bu\delta_A^{-1}$ and $h=\eta_B^{-1}G(v)\eta_A$; naturality of $\varepsilon$ gives $Fh=\delta_B^{-1}v\delta_A=u$, so $F$ is full.

For each $A$, fullness gives a unique $\eta_A:A\to GFA$ with $F(\eta_A)=\varepsilon_{FA}^{-1}$; faithfulness and naturality of $\varepsilon$ make $\eta$ natural, and [L3] makes each $\eta_A$ an isomorphism because its image is.

Thus $(F,G,\eta,\varepsilon)$ is equivalence data. The two constructions prove both directions without making any unrecorded selection.