As I’ve been working through “Sheaves in Geometry and Logic”, I’ve been skimming proofs and attempting to rederive them. I normally end up with a better understanding of the material, but sometimes I get stuck. Here’s one case where I’ve gotten stuck: can anybody tell me why the counit for the exponential is universal? In particular, I can’t manage to show the uniqueness of at the end of the proof. I started this entry back in April, and figured I should finally finish it off and ask for help.

Theorem. Given any small category , the presheaf category is Cartesian closed.

Proof. We must show that has a terminal object , finite products, and exponentials.

The terminal is given by the constant functor onto in .

The product of is given pointwise, that is, .

So it remains to find an exponential . Recall that, by analogy with the motivating example in , we define exponentiation to be right adjoint to the right product, explicitly, . In particular, for all , we want

natural in and .

A first guess of fails to work in any sensible functorial way (it’s not at all clear what should be).

Suppose now that is representable. Then there exists a such that . Then (*) becomes

But by the Yoneda lemma, assuming exists,

So we make an educated guess and define

and for , let be given by

That’s to say, for any ,

So we’ve defined on objects. Now we must define for arrows of . What we need is a natural transformation , that is, a family of arrows of . Here, we make use of our intuition from and define:

It is straightforward to check that is a natural transformation, that is, for each in , we have

Indeed, given a , going around the top right side of the square gives

while going around the bottom left side of the square gives

Now that we have a candidate for , we need to show that it is actually an exponential, that’s to say, that for all , we have the adjunction . We do so by means of a counit . Observe that in , this counit is exactly function evaluation, i.e., is given by . Hence why we call the counit “evaluation”.

Recall that a counit for an adjunction is a “natural transformation such that each arrow is universal from to while each has left adjunct ” [CWM].

So to show that is a counit for , we must show that it is a natural transformation such that is universal from to . That’s to say, for every , we must have a unique such that the following triangle commutes:

We see that our choices are heavily constrained by the types at hand. For every , we need a natural transformation , i.e., a family , i.e., a family of morphisms in . So each receives a pair ,

and must produce an . The only arrow into we know must exist is the identity . Observe also that . So we take

Though we were in a sense “forced” to make this definition by the types, we must still check that is a natural transformation. Let be arbitrary in . We must show that

To see why , first observe:

But is natural, so we have , in particular, that . So by transitivity, we have the desired equality in the bottom right corner of the naturality diagram. So we conclude that is a natural transformation and is thus eligible to be component of the (candidate) natural transformation . (There is no confusion here: because the morphisms of are natural transformations, the components of , being arrows of , are natural transformations. To the best of my understanding, this is an instance of a 2-category.) We must now show that is a natural transformation between the functors and . Let and be arbitrary objects (functors) in and let be an arbitrary morphism (natural transformation) between them. Then we want to show that the following diagram commutes:

This diagram commutes if and only if for every object in , the following diagram commutes in :

Given a pair , going around the top right corner of the square gives us

while going around the bottom left gives us

So we can finally conclude that is a natural transformation.

Let’s briefly recap what we’ve accomplished so far and where we’re trying to go. We’re trying to show that has exponents, that’s to say, a right adjoint . We’ve found a candidate functor , as well as a natural transformation . All that remains is to show that is a counit for the adjunction. This involves finding for every a unique such that the above-given triangle commutes.

So we need for all , , ,

where is a natural transformation. So we must find a family of maps

natural in . Let’s draw inspiration from the types at hand: again they will force our hand.

So the obvious candidate is:

Let’s check commutativity:

So the triangle commutes as desired.

Checking naturality is straightforward.

All that remains is to show the uniqueness of . And this, dear reader, is where I’m stuck. Any hints would be greatly appreciated, please comment below!