proposition: Lemma natural_from_component : naturality (codensityT M) M from_component.
proof: Proof. move=> A B h; apply funext => m /=. rewrite [RHS](_ : _ = m B (Ret \o h)) //. rewrite -natural. rewrite [LHS](_ : _ = (M # h \o m A) Ret) //. by rewrite naturality_MK. Qed.
imports: mathcomp(all_ssreflect) HB(structures) imonae_lib ihierarchy imonad_lib imonad_transformer