Theorem: For categories and , is isomorphic to .
Proof: We’ll first need to define a functor . Let be an object of – that is a functor . Then, let be a functor such that for an object , , and for an arrow of , (flip the arrow, send it through , and flip it again).
Now, having described what does to objects in (functors), we need to describe what does to arrows (natural transformations). If is a natural transformation between , We need to be natural transformation between . For , notice that is an arrow in whose domain is and whose codomain is . So we can just define , which is an arrow in whose domain is and whose codomain is . Then, we have a well-defined map for each , and is a natural transformation as prescribed.
We quickly verify that is indeed a functor. If is the identity natural transformation on , then
Suppose are natural transformations. Then we have
(composed in the opposite order because is contravariant).
One can obtain the inverse functor by applying the identical construction starting with and . In this way, we get a functor . But, this can equally well be described as a functor . Either way, is defined by identical rules to . If , recall and . So, and . So, . If is a natural transformation, recall that we have . So, . So . Together, this means that is the identity functor on . It follows symmetrically that is the identity on . Thus, and are isomorphic.