fact: Definition kappa' : E ~~> codensityT M := fun (A : UU0) (s : E A) (B : UU0) (k : A -> M B) => op B ((E # k) s).
imports: mathcomp(all_ssreflect) HB(structures) imonae_lib ihierarchy imonad_lib imonad_transformer