> Equational presentation would be great to see. Maybe that would help me to better parse Haskell. I'm more comfortable with the straight mathematical language, and with "ordinary" languages like Python, but when I look at Haskell code it can look blurry.

I have to admit I really like Haskell and I think its great for studying category theory. Equational reasoning in Haskell is quite common in research papers.

That being said, I'll try to balance these discussions with more traditional mathematics.

Anyhow, here's the usual commutative diagram for the coproduct:


The diagram doesn't mention the morphism composition operation \\((\nabla) : (A \to C) \Rightarrow (B \to C) \Rightarrow A + B \to C\\), but it takes the place of \\(f\\). Instead of \\(f\\), we would write \\(f_1 \nabla f_2\\).

The morphism composition operation \\((\nabla)\\) is unique in obeying the equations for the coproduct, are quite similar to the product equations:

f \nabla g \cdot i_1 = f\\\\
f \nabla g \cdot i_2 = g\\\\
(f \cdot i_1) \nabla (f \cdot i_2) = f

In *Hask*, \\(i_1\\) is `Left :: a -> Either a b`, \\(i_2\\) is `Right :: b -> Either a b`, and \\((\nabla)\\) is `either :: (a -> c) -> (b -> c) -> Either a b -> c`

Once again, I feel the only real challenge in the case of *PreOrder* is showing all of the morphisms involved are order preserving maps. I did something similar above so I'll just wave my hand at that.


The adjunction \\( \bullet \times A \dashv \bullet^A \\) is realized by the functors `(,a)` and `(->) a`. That second functor is called the _reader monad_. It comes up pretty often when you have to read information from a config for a web app and you don't want to carry a parameter around.

The isomorphism `Hom(- \times A, B) \simeq Hom(-, B^A)` is realized by two functions:

uncurry :: (c -> a -> b) -> (c,a) -> b
curry :: ((c,a) -> b) -> (c -> a -> b)

Okay, it's getting a bit late, more tomorrow...

[EDIT: Formatting, mentioning uniqueness]