proposition: Lemma naturality : naturality [the functor of (exponential_F A \o M)] M m.
proof: Proof. move=> X Y f /=; apply funext => eX. set rhs := RHS. have : Ml_R X Y (fun x y => f x = y) (m X eX) rhs. apply: param => a _ <-; rewrite Actm_exponenial_FE compE. by elim: (eX a) => [|? ? ?]; constructor. by rewrite compE; elim => // x _ <- l _ _ <-. Qed.
imports: Param(Param) mathcomp(all_ssreflect) HB(structures) imonae_lib ihierarchy imonad_lib ifmt_lifting imonad_model