On Wed, 2008-08-06 at 13:56 -0700, Jason Dusek wrote:

The problem as stated is to find the unit for the adjunction:

((- x A), (-)^A x A)

The latter functor takes an arrow f to (f . -) x id_A and does the obvious thing for objects. The co-unit diagram is given as:

B^A x A ---- eval_AB ----> B ^ ^ | | | | curry(g) x id_A g : C x A -> B | | | | | | C x A --------------------+

This diagram is somewhat puzzling, because it seems the second functor has turned into (-)^A ! Continuing in with that, we get a unit diagram like this:

C ---- magic ----> (C x A)^A | | | | | | curry(g) (g . -) | | | | | v +------------------> B^A

So what is the magic? It is an arrow that takes a C to an arrow that takes an A and makes the product C x A. I want to write curry(C x A) but that is ridiculous looking. What's the right notation for this thing?

It's a curried pairing operator. Haskell calls it (,); it might also be called pair. It is also, of course, equal to curry(id), so if you write identity arrows as the corresponding objects then curry(C x A) is perfectly reasonable. (This function is rather fundamental, meaning its main purpose is to justify a move that, 99% of the time it's made, is made without any comment at all. Spelling it out /is/ ridiculous, in the same sense that explicitly invoking modus ponens in your proofs is ridiculous. Unless you're doing low-level formal proof theory, of course.) jcc