| context | ${\bf C},{\bf D}$ … categories |
| definiendum | $F$ in ${\bf D}\simeq{\bf C}$ |
| inclusion | $F$ in ${\bf D}\longrightarrow{\bf C}$ |
| exists | $G$ in ${\bf C}\longrightarrow{\bf D}$ |
| exists | $\alpha$ in $FG\cong Id_{\bf C}$ |
| exists | $\beta$ in $Id_{\bf D}\cong GF$ |
Here $Id_{\bf C}$ denotes the identity functor on ${\bf C}$.
We want to formalize when two categories are “exchangeable in terms of results which can be workout in them”. We would call a functors $F$ “invertible” if there is a another functor $G$ so that $G\circ F=Id_{\bf D}$ and $F\circ G=Id_{\bf C}$. However, since one is generally interested in statements involving objects up to isomorphism only, we define a functor to give an “equivalence” by the above definition.
Comparison with homotopy theory: The postulate then looks essentially the same as the one for homotopy equivalent spaces. The natural transformations $\alpha,\beta$ play the role of homotopy equivalences. Working up to isomorphism amounts to working with just any one representative of a homotopy type.
See also my equivalence of categories.
Wikipedia: Equivalence of categories