proposition: Lemma naturality_kappa' : naturality _ _ kappa'.
proof: Proof. move=> A B h; rewrite /kappa'; apply funext => ea; rewrite [in RHS]/=. transitivity (fun B0 (k : B -> M B0) => op B0 ((E # (k \o h)) ea)) => //. by apply funext_dep => C; apply funext => D; rewrite functor_o. Qed.
imports: mathcomp(all_ssreflect) HB(structures) imonae_lib ihierarchy imonad_lib imonad_transformer