proposition: Lemma slifting_outputT (X : UU0) : (slifting op [the fmt of outputT R] naturality_MK) X = @op' _.
proof: Proof. apply funext => emx. rewrite /op'. rewrite /slifting. rewrite 2!vcompE. set h := hmap _. rewrite (psikE op). rewrite 2!functor_app_naturalE. rewrite /=. f_equal. rewrite /psi' /= /bindK /bindO /= bindE /= /bindK /=. apply funext_dep => A; apply funext => f. rewrite fmapE /bindK. rewrite vcompE/=. rewrite /liftO /=. rewrite -(compE _ _ emx) -functor_o. rewrite bindE /= /bindK /=. rewrite fmapE. rewrite /bindK. rewrite /psi' /= /bindK /= /kappa' /=. congr (op A). rewrite -(compE _ _ emx) -[in RHS](compE _ _ emx). rewrite -2!functor_o. congr ((E # _) _). apply funext => rmx /=. rewrite /retK /= bindE fmapE /= /bindK. congr (Lift [the monadT of codensityT] M _ _ _ _). by apply funext => -[]. Qed.
imports: mathcomp(all_ssreflect) HB(structures) imonae_lib ihierarchy imonad_lib imonad_transformer