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