proposition: Lemma naturality : naturality [the functor of (exponential_F A \o M)] M m.
proof: Proof. move=> X Y f; apply funext => eX. by apply (param X Y (fun x y => (M # f) x = y)) => a _ <-. Qed.
imports: Param(Param) mathcomp(all_ssreflect) HB(structures) imonae_lib ihierarchy imonad_lib ifmt_lifting imonad_model