[Haskell-cafe] adjoint of coproduct & diagonal

[Derek Elkins]

On Sat, 2008-08-02 at 18:22 -0700, Jason Dusek wrote:
> I'm trying to figure out the adjunction diagrams for the
>   adjunction where the diagonal functor is right adjoint to the
>   coproduct functor. I'm |almost done|, but the co-unit has me
>   stumped, because I can't figure out how the arrow at the top
>   can be unique -- it seems it could be either one of:
> 
>     i_1 . [f,g]
>     i_2 . [f,g]
> 
>       i_1, i_2 : C -> C+C
>       f : A -> C
>       g : B -> C
> 
>   The net effect of [id,id] on the right is to blur out the
>   distinction. On #haskell, someone suggested there is a
>   constraint I am missing; I've poked around for a day and still
>   can't figure it out.

[id,id] is the counit.
[id,id] : C+C -> C
Given a function f : A+B -> C there exists a unique function
f* : (A,B) -> (C,C) that is a pair of functions
h : A -> C and k : B -> C such that
[id,id] . h+k = f.
The one way is obvious given f, h = f . inL and k = f . inR
So a solution exists.
To show that it is unique assume we are given an h and k such that the
above equation holds we need to show that h = f . inL (and similarly for
k.)
So start by precomposing both sides of the equation with inL giving:
[id,id] . h+k . inL = f . inL
We simply need to show that the left side is h.  The injections together
form the unit.  Naturality of the unit says that for any h and k:
h : A -> B
k : C -> D
inL . h = h+k . inL
inR . k = h+k . inR
Using this in the above we have:
[id,id] . inL . h = f . inL
Now we use one of the triangle identities which states:
[id,id] . inL = id
[id,id] . inR = id
and this finishes the proof:
id . h = f . inL
h = f . inL