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 $\epsilon :FG\Rightarrow 1_{\mathcal{D}}$. Then $D\mapsto (GD,{\epsilon }_D)$ explicitly splits essential surjectivity.

Conversely, assume $F$ is fully faithful and comes with objects $C_D$ and isomorphisms ${\epsilon }_D:F{C}_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 ${\epsilon }_E^{-1}u{\epsilon }_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 $\epsilon :FG\Rightarrow 1_{\mathcal{D}}$.

Put ${\delta }_A={\epsilon }_{FA}\circ F({\eta }_A)$, an automorphism of $FA$. For $u:FA\to FB$, set $v={\delta }_{B}u{\delta }_A^{-1}$ and $h={\eta }_B^{-1}G(v){\eta }_A$; naturality of $\epsilon$ 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)={\epsilon }_{FA}^{-1}$; faithfulness and naturality of $\epsilon$ make $\eta$ natural, and [L3] makes each ${\eta }_A$ an isomorphism because its image is.

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