@Matthew I've continued working with my puzzle about the relations between the proofs about adjunctions over posets in the book and implementations of the adjunctions in Haskell. *Exercise 1.91* in the book asks us to prove, using *Proposition 1.81*, that if \\(f \dashv g \\) then:

1. \\( p \le g(f(p)) \\)
2. \\( g(f(g(f(p)))) \cong g(f(p)) \\)

Let's beging with 1. From the Haskell perspective, this expression is similar to the `unit` (a.k.a. `return`) of a monad.

1'. `unit :: a -> g (f a)`

The proof of 1. is given by reflexivity \\( f(p) \le f(p) \\) and then adjointness \\(p \le (g(f(p)) \\)

The implementation of `unit` is giving by

`unit = leftAdjoint id`

which has exactly the same structure as the proof of 1 (`id` is the translation of _reflexivity_ into the Haskell domain).

Let's return to the 2, which is

\\( g(f(g(f(p)))) \cong g(f(p)) \\)

We have to prove it in both directions:

2a. \\( g(f(g(f(p)))) \le g(f(p)) \\)

From 3. we have \\( f(g(q)) \le q \\); by monotonicity of \\( g \\) we get \\( g(f(g(q))) \le g(q) \\); which is valid for all \\( q \in Q \\) and in particular for \\( q = f(p) \\) so \\( g(f(g(f(p)))) \le g(f(p)) \\).

Its Haskell version is the function `join` (part of the definition of a monad)

2a'. `join :: g (f (g (f a))) -> g (f a)`

and its implementation

`join :: fmap counit`

2b. \\( g(f(p)) \le g(f(g(f(p)))) \\)

From 1. we have \\( p \le g(f(p)) \\); by monotonicity of \\( f \\) we get \\( f(p) \le f(g(f(p))) \\); and by monotonicity of \\( g \\) we get \\( g(f(p)) \le g(f(g(f(p)))) \\)

Its Haskell version is the `duplicate'` function (the name is due that it has the structure of the `duplicate` function of a comonad)

2b'. `duplicate' :: g (f a) -> g (f (g (f a)))`

and its implementation is given by

`duplicate' = (fmap . fmap) unit`.

A footnote before *Exercise 1.91* tells us that we can do the same "the other way round", that is, that we can similarly prove

3. \\( f(g(q)) \le q \\)
4. \\( f(g(f(g(q)))) \cong f(g(q)) \\)

Which, in the Haskell domain, seems very similar to `counit` (a.k.a. `extract`) in a comonad. I'll omit the proofs because are dual to the ones presented.

3'. `counit :: f (g a) -> a`

and an implementation

`counit = rightAdjoint id`

From the proof of 4 we get

4a'. `join' :: f (g (f (g a))) -> f (g a)`


4b'. `duplicate :: f (g a) -> f (g (f (g a)))

with implementations:

join' = (fmap . fmap) counit
duplicate = fmap unit

So we have proved that given \\(f \dashv g \\), \\(g \circ f\\) is a *monad* (with `unit` and `join`) and that \\(f \circ g\\) is a *comonad* (with `extract` and `duplicate`).

I don't know if the other two functions, `join'` and `duplicate'`, give any interesting properties to \\(f \circ g\\) and \\(g \circ f\\).

PS: I haven't proved if the equations which relate `unit` and `join` in a monad (resp. `counit`and `extract` in a comonad) follow from their implementations.