An isomorphism of categories is a pair of functors
such that we have
Categories can be equivalent but non-isomorphic. For example, the category consisting of two isomorphic objects is equivalent to $\mathsf{pt}$, but not isomorphic to it.
Let $F\colon \mathcal{C}\to \mathcal{D}$ be a functor.
For each $X\in \operatorname {\mathrm{Obj}}\webleft (\mathsf{Cats}\webright )$, the precomposition functor
is an isomorphism of categories.
For each $X\in \operatorname {\mathrm{Obj}}\webleft (\mathsf{Cats}\webright )$, the postcomposition functor
is an isomorphism of categories.
Item 1a and Item 1b Are Equivalent: Omitted, but similar to Item 1 of Proposition 11.6.7.1.2.
Item 1a, Item 1c, and Item 1d Are Equivalent: This follows from 
.
This finishes the proof.
