proposition: Lemma slifting_stateT (X : UU0) : (slifting op [the fmt of stateT S] naturality_MK) X = @op' _.
proof: Proof. apply funext => emx. rewrite /op'. apply funext => s. rewrite /slifting. rewrite 2!vcompE. set h := hmap _. rewrite [in RHS](psikE op). rewrite 2!functor_app_naturalE. rewrite /=. congr (from_component _). apply funext_dep => A; apply funext => f. rewrite {1}/psi' /=. rewrite /bindS /=. rewrite vcompE/=. rewrite /liftS /=. rewrite bindA. set ret_id := (X in _ >>= X). have -> : ret_id = fun (x : MS S (codensityT M) X) (C : UU0) => (fun t => x s C t). by apply funext. rewrite /psi' /= /bindK /kappa' /=. congr (op A). rewrite -2![in LHS](compE _ _ emx) -2![in RHS](compE _ _ emx). by rewrite -!functor_o. Qed.
imports: mathcomp(all_ssreflect) HB(structures) imonae_lib ihierarchy imonad_lib imonad_transformer