fact: Definition localT (f : Env -> Env) : T M ~~> T M := fun X t => let t' := hmap T (Lift [the monadT of codensityT] M) X t in hmap T (from naturality_MK) X (localKT f t').
imports: mathcomp(all_ssreflect) HB(structures) imonae_lib ihierarchy imonad_lib imonad_transformer imonad_model