First off, the arrows that we used to read off the -component of a natural transformation turn out to fit into a more general structure. As we might hope there’s an “evaluation” functor that takes a -functor from to and evaluates it on an object of to give an object of . The partial functors are and . That this is actually a -functor follows yet again from that litany of naturalities we keep referring to.
Now the -functor induces an ordinary functor . Remember here that is a 2-category — a category enriched over ordinary categories — so each hom-object is a category, and an arrow from one hom-object to another is a functor. In particular, given a functor we get a functor . And then we compose with the evaluation functor to get a functor . It turns out that this functor is an isomorphism of categories.
This means that every functor is of the above form for some unique . Let’s look at the partial functors of and .
The first of these equations completely determines the functor in that must assign to an object of . The second uniquely determines the action of on hom-objects because is the counit of an end, and it comes with a universal property. Thus the above map is bijective on objects. But since it’s a functor we also need it to be bijective on morphisms — natural transformations in this case.
So, if we’ve got functors and from to , with images and from . Now we need to check that every -natural is of the form for some unique -natural . But by the equation above between the second partial functors, this says that . Thus is the -natural transformation .
We now have a 2-natural isomorphism (natural isomorphism enriched over ): . Equivalently, this means that is 2-natural in each variable. Using this naturality it’s straightforward to show that given and we get a -functor by composing functors.
All of this fits together to say that the 2-functor has a right adjoint when exists for all . At this point, the existence tends to hinge on a lot of smallness technicalities. The 2-category of all -categories is thus “partially closed”, in a similar way to the 2-category of all ordinary categories. However, if we restrict to small -categories we actually do have a symmetric, monoidal, closed 2-category.
In either case, partial closedness together with the Fubini theorem is enough for us to get the standard isomorphisms and . This latter holds in the sense that either side exists if the other one does.