proposition: Lemma from_component_liftK A : @from_component A \o Lift [the monadT of codensityT] M A = id.
proof: Proof. by apply funext => m /=; rewrite /from_component/= /liftK /= bindmret. Qed.
imports: mathcomp(all_ssreflect) HB(structures) imonae_lib ihierarchy imonad_lib imonad_transformer