fact: Definition naturality_MK (M : functor) (A : UU0) (m : MK M A) := naturality [the functor of exponential_F A \o M] M m.
imports: mathcomp(all_ssreflect) HB(structures) imonae_lib ihierarchy imonad_lib imonad_transformer