proposition: Lemma muM_natural : naturality _ _ mu.
proof: Proof. move => A B h. rewrite (_ : [the functor of M \o M] # h = g # ([the functor of f \o g] # (f # h))) //. rewrite (_ : _ \o g # ([the functor of f \o g] # (f # h)) = g # (@eps (f B) \o ([the functor of f \o g] # (f # h)))); last by rewrite -functor_o. rewrite -natural FIdE. rewrite [in LHS]FCompE. rewrite /mu. by rewrite -[in LHS](@functor_o g). Qed.
imports: ssrmatching mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy