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

$$\begin{eqnarray} f(a) \vee f(b) & \leq & f(a \vee b) \\\\ f(a \wedge b) & \leq & f(a) \wedge f(b) \\\\ \end{eqnarray}$$

-------------------------------------

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.