proposition: Lemma slifting_alifting_outputFMT (R : UU0) (t := [the fmt of outputT R]) : slifting aop t naturality_MK = alifting aop (Lift t M).
proof: Proof. apply nattrans_ext => X. rewrite (slifting_outputT aop naturality_MK R). apply funext => m. rewrite /alifting. rewrite /=. rewrite psiE /= /bindO. rewrite vcompE/=. rewrite /liftO. rewrite 2!algebraic. congr (aop _ _). rewrite -[RHS](compE _ (E # _)). rewrite -functor_o. rewrite -[RHS](compE _ (E # _)). rewrite -functor_o. rewrite (_ : _ \o Ret = id) ?functor_id //. apply funext => n /=. rewrite 2!bindretf. Open (X in _ >>= X). by case : x => ? ?; rewrite cat0s. by rewrite bindmret. Qed.
imports: mathcomp(all_ssreflect) HB(structures) imonae_lib ihierarchy imonad_lib imonad_transformer