Let and be categories.
An equivalence between and consists of Functors:

and Natural Isomorphisms:

We write if there exists such an equivalence.

Lemma

Let be a Functor.
Then is part of an equivalence
if and only if
is Full, Faithfull and Essentially Surjective.

Proof

Suppose we are given a Functor
and Natural Isomorphisms and .
For any ,
is an Isomorphism
so is Essentially Surjective
Given in , note
so is recoverable from , and
i.e. is unique given , and
i.e. is Faithfull.
Suppose there is some .
The composite:

satisfies:

Note that is Faithfull for the same reason as
so we get .

For each choose an Object of
and an Isomorphism in ,
which we can do as is Essentially Surjective.
Given in consider

and define to be the unique Morphism such that

which we can do as is Full (existence) and Faithfull (uniqueness)

Uniqueness implies functoriality:
given , and have the same image under
so they’re equal.
By construction, is a Natural Isomorphism
Define to be the unique Morphism
whose inverse under is

As we already saw, is an Isomorphism for all ,
and Naturality Squares for are mapped by
to naturality squares for so they commute.

Example

Category of Partial Functions is equivalent to
the category of pointed sets.
We define by

defined by if , undefined otherwise
and by

Then and there is a Natural Isomorphism
sending to
Note that has a singleton isomorphism class of objects ,
but doesn’t so .

Example

The Category of finite dim Vector Spaces over ,
is equivalent to using the Dual Space Functor and the Natural Transformation

Example

is also equivalent to
the functor sends to
and a matrix to the linear map
which it represents wrt the standard bases
To define , choose a basis for each finite dim space,
and define and matrix representing w.r.t the chosen basis
Now provided we choose the standard bases for the spaces
but the chosen basis for yields an isomorphism
and these form a Natural Transformation isomorphism