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

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