proposition: Theorem uniform_sigma_lifting : lifting_monadT op slifting.
proof: Proof. rewrite /lifting_monadT /slifting => X. apply/esym. transitivity ((op1 \v op2) X \o op3 X \o E # Lift t M X). by rewrite (vassoc op1) vcompE/= !vcompE. rewrite -compA. transitivity ((op1 \v op2) X \o ((E # Lift t (codensityT M) X) \o (E # Lift [the monadT of codensityT] M X))). congr (_ \o _); rewrite /op3. by rewrite -functor_o -natural_hmapE functor_app_naturalE -(@functor_o E). transitivity (op1 X \o (op2 X \o E # Lift t (codensityT M) X) \o E # Lift [the monadT of codensityT] M X). by rewrite vcompE -compA. rewrite -uniform_algebraic_lifting. transitivity (Lift t M X \o from naturality_MK X \o (psik op) X \o E # Lift [the monadT of codensityT] M X). congr (_ \o _). by rewrite compA natural_hmapE. rewrite -2!compA. congr (_ \o _). by rewrite compA -psikE. Qed.
imports: mathcomp(all_ssreflect) HB(structures) imonae_lib ihierarchy imonad_lib imonad_transformer