One relation between the haskell code for the Adjunction typeclass and the Galois connections in the text is, for example, the proof that \\( p \le g(f(p)) \\).
The proof starts with \\( f(p) \le f(p) \\), and then applies the adjunction to get \\( p \le g(f(p)) \\).
In Haskell this corresponds to the implementation of the `unit` function
unit :: a -> g(f(a))
unit = leftAdjunction id
Being `unit` the same function as the monad's `return` (modulo use of `Comp1`)
return = Comp1 . unit
**What property of the Galois connection is proved by the implementation of bind `(>>=)` ?**
x >>= f = Comp1 (fmap (rightAdjunct (unComp1 . f)) (unComp1 x))