I've been playing around with the relationship between monoids and monads (see http://www.jonmsterling.com/posts/2012-01-12-unifying-monoids-and-monads-wit... http://blog.sigfpe.com/2008/11/from-monoids-to-monads.html), and I put together my own implementation which I'm quite happy with, that you can see at http://hpaste.org/56903 ; relying only on the extensions RankNTypes, TypeOperators, NoImplicitPrelude, ScopedTypeVariables; At the end of that paste, I prove the three Haskell monad laws from the functor laws and "monoid"-ish versions of the monad laws, but my proofs all rely on a property of natural transformations that I'm not sure how to prove; given type m :-> n = (forall x. m x -> n x) class Functor f where fmap :: forall a b. (a -> b) -> f a -> f b -- Functor identity law: fmap id = id -- Functor composition law fmap (f . g) = fmap f . fmap g Given Functors m and n, natural transformation f :: m :-> n, and g :: a -> b, how can I prove (f . fmap_m g) = (fmap_n g . f)? Is there some more fundamental law of natural transformations that I'm not aware of that I need to use? Is it possible to write a natural transformation in Haskell that violates this law? -- ryan