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 _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
