@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).

\$$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)

and

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. counitand extract` in a comonad) follow from their implementations.