Essential surjectivity
= Essential surjectivity
A <functor> $F:\mathcal C\to\mathcal D$ is essentially surjective when every object of $\mathcal D$ is isomorphic to $FA$ for some $A\in\mathcal C$. Together with <full and faithful>, this characterizes an <equivalence of categories> under the appropriate <axiom of choice> convention. For large categories, choosing a quasi-inverse on all objects requires a universe or a class-choice convention.