proposition: Lemma Actm_exponenial_FE (M : monad) (X Y : UU0) (f : X -> Y) : forall A eX, ([the functor of (exponential_F A \o M)] # f) eX = M # f \o eX.
proof: Proof. by []. Qed.
imports: Param(Param) mathcomp(all_ssreflect) HB(structures) imonae_lib ihierarchy imonad_lib ifmt_lifting imonad_model