Hmm... let me say my thinking. Taking what you just wrote, we actually have:

introduceCoproduct :: Functor f => Either (f a) (f b) -> f (Either a b)
introduceCoproduct = fmap Left ||| fmap Right

extractProduct :: f (a, b) -> (f a, f b)
extractProduct = fmap fst &&& fmap snd

These reflect that, for every monotone \\(f\\):

f(a) \vee f(b) & \leq & f(a \vee b) \\\\
f(a \wedge b) & \leq & f(a) \wedge f(b) \\\\


The Galois connections in Fong and Spivak are defined to be between two preorders \\(\leq_A\\) and \\(\leq_B\\).

On the other hand, Ed Kmett's adjunctions are always between `Category (->)` and `Category (->)`.

This restricts us from looking at one of the cutest adjunction constructions I know. *If we have a Monad `m`, we compute two adjunctions!* It's a classic construction. I don't think it's in Fong and Spivak :( It is at the heart of the `>=>` operator in Haskell if you've ever used it.

However, I think I know why Kmett came up his adjunctions library the way he did. He has *another* adjunction construction he came up with 10 years ago. But his is all in `Category (->)`.

I can talk about these if you like.