Equivalence of categories

An equivalence consists of functors $F:\mathcal{C}\to \mathcal{D}$ and $G:\mathcal{D}\to \mathcal{C}$ with natural transformation isomorphisms $GF\cong 1_{\mathcal{C}}$ and $FG\cong 1_{\mathcal{D}}$. A full and faithful functor which is essentially surjective, meaning every target object is isomorphic to an image object, is part of an equivalence under the usual choice convention. An isomorphism of categories is stronger: it has a strictly inverse functor.

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.

An isomorphism of categories is a functor with a strictly inverse functor. It is equivalently bijective on objects and on each hom-set. An equivalence of categories only requires inverse composites up to invertible natural transformations. For example, the category of partial functions and the category of pointed sets are equivalent but their actual object collections prevent an isomorphism: the former has one zero object, the empty set, while the latter has distinct singleton pointed set objects that are all zero objects.