Derek Elkins derek.a.elkins at gmail.com
Sun Dec 14 18:52:14 EST 2008

```On Mon, 2008-12-08 at 23:15 +0100, Joachim Breitner wrote:
> Hi,
>
> Am Montag, den 08.12.2008, 15:59 -0600 schrieb Nathan Bloomfield:
>
> > Slightly off topic, but the A^B notation for hom-sets also makes the
> > natural isomorphism we call currying expressable as A^(BxC) = (A^B)^C.
>
> So A^(B+C) = A^B × A^C ?
>
> Oh, right, I guess that’s actually true:
>
> uncurry either                :: (a -> c, b -> c)  -> (Either a b -> c)
> (\f -> (f . Left, f . Right)) :: (Either a b -> c) -> (a -> c, b -> c)
>
> It’s always nice to see that I havn’t learned the elementary power
> calculation rules for nothing :-)

I want to point out a quick categorical way of proving this (and almost
all the other "arithmetic" laws follow similarly.)  This is just
one that is commonly neglected in discussions of Cartesian closed
categories.

A^- is a function C^{op} -> C and it is adjoint to itself on the right,
i.e. (A^-)^{op} -| A^-.  As an isomorphism of hom functors that is,
Hom(=,A^-) ~ Hom(-,A^=) or in Haskell notation there is an isomorphism
flip :: (a -> b -> c) -> (b -> a -> c) (it is it's own inverse.)  This
is induced by the swap operation on pairs and is why for enriched
categories usually they talk about -symmetric- monoidally closed
categories.  Symmetric monoidally closed categories validate all the
arithmetic laws as well.

So B+C is BxC in the opposite category and so A^- takes (BxC)^op to A^B
x A^C.

And that's not all, every adjunction gives rise to a monad namely,
A^(A^-) or in Haskell notation (b -> a) -> a and indeed if you work out
the details this is the continuation monad.

```