I hope this is the right place to write this.

I was thinking about Fong and Spivak's first chapter, where they focus on [Galois connections](https://en.wikipedia.org/wiki/Galois_connection). Galois connections are a special case of [*adjunctions*](https://en.wikipedia.org/wiki/Adjoint_functors), where the functors are acting over two posets.

I thought it might be fun to do an exercise in Haskell based on Ed Kmett's [adjunction](https://hackage.haskell.org/package/computational-algebra-0.3.0.0/docs/Data-Functor-Adjunction.html) library.

In Haskell, we can write an adjunction between two _endofunctors_ as a type class. This type class has two natural transformations:

In category theory, this is written as \\(f \dashv g\\)

In this class,

**Puzzle 1**: Give the type class instance for

**Puzzle 2**: Define

**Puzzle 3**: Give a definition of

**Puzzle 4**: Check out the [_functor composition type constructor_ (:.:)](https://hackage.haskell.org/package/base-4.11.0.0/docs/GHC-Generics.html#t::.:), and consider

I was thinking about Fong and Spivak's first chapter, where they focus on [Galois connections](https://en.wikipedia.org/wiki/Galois_connection). Galois connections are a special case of [*adjunctions*](https://en.wikipedia.org/wiki/Adjoint_functors), where the functors are acting over two posets.

I thought it might be fun to do an exercise in Haskell based on Ed Kmett's [adjunction](https://hackage.haskell.org/package/computational-algebra-0.3.0.0/docs/Data-Functor-Adjunction.html) library.

In Haskell, we can write an adjunction between two _endofunctors_ as a type class. This type class has two natural transformations:

`leftAdjunct`

and `rightAdjunct`

.

{-# LANGUAGE MultiParamTypeClasses #-}

{-# LANGUAGE FunctionalDependencies #-}

{-# LANGUAGE Rank2Types #-}

{-# LANGUAGE TypeOperators #-}

module Adjunction where

import GHC.Generics

class (Functor f, Functor g) => Adjunction f g | f -> g, g -> f where

leftAdjunct :: (f a -> b) -> a -> g b

rightAdjunct :: (a -> g b) -> f a -> b

In category theory, this is written as \\(f \dashv g\\)

In this class,

`leftAdjunct`

and `rightAdjunct`

are natural transformations and obey the following laws:

-- leftAdjunct . rightAdjunct === id

-- rightAdjunct . leftAdjunct === id

**Puzzle 1**: Give the type class instance for

`Adjunction ((,) e) ((->) e)`

**Puzzle 2**: Define

`unit :: Adjunction f g => a -> g (f a)`

and `counit :: Adjunction f g => f (g a) -> a`

such that:

-- leftAdjunct counit === id

-- rightAdjunct unit === id

**Puzzle 3**: Give a definition of

`leftAdjunct`

and `rightAdjunct`

in terms of `unit`

and `counit`

(so now we can write `{-# MINIMAL (unit, counit) | (leftAdjunct, rightAdjunct) #-}`

when we define the `Adjunction`

type class).**Puzzle 4**: Check out the [_functor composition type constructor_ (:.:)](https://hackage.haskell.org/package/base-4.11.0.0/docs/GHC-Generics.html#t::.:), and consider

`Comp1 . unit :: Adjunction f g => a -> (g :.: f) a`

. Write out `instance Adjunction f g => Monad (g :.: f)`

where `return = Comp1 . unit`

. What popular monad is this isomorphic to in the special case of `Adjunction ((,) e) ((->) e)`

?