proposition: Lemma psikE (A : UU0) : op A = (@from_component M A) \o (@psik A) \o ((E ## Lift [the monadT of codensityT] M) A).
proof: Proof. apply funext => m /=. rewrite /from_component /psik /= /psi' /kappa' /fun_app_nt /=. rewrite /bindK /=. rewrite -[in RHS]compE. rewrite -[in RHS]compE. rewrite -compA. rewrite -functor_o. rewrite from_component_liftK. rewrite functor_id. by rewrite compfid. Qed.
imports: mathcomp(all_ssreflect) HB(structures) imonae_lib ihierarchy imonad_lib imonad_transformer