§ Adjunctions as advice

An adjunction F |- U allows us to go from F a -> x to a -> U x. We can look at this as shifting the "before-advice" from the input to an "after advice" of the output , where I'm using Also, to remember this, we can write it as: 
F a <--F--- a
|           |
v           v
x ----U--> U x
Where F is for Free and U is for forgetf Ul. Recall that if F is free and U is forgetful, then U(F(x)) = x, since adding more structure through the free functor and then stripping it away gives us the object back. We can prove that if U(F(x)) = x and U, F are functors, then we have a function fwd: (f a -> x) -> (a -> u x) as: 
f      :: (f a -> x)
fmap   :: (p   -> q) -> (u p     -> u q)
fmap   :: (p   -> q) -> (u ( p ) -> u q)
fmap f :: (f a -> x) -> (u (f a) -> u x)
fmap f :: (f a -> x) -> (a       -> u x) [using u (f a) = a]

§ References