proposition: Lemma naturality_ret : naturality FId [the functor of M \o N] ret_comp.
proof: Proof. by move=> A B h; rewrite -(natural ((@ret M) \h (@ret N))). Qed.
imports: mathcomp(all_ssreflect) HB(structures) imonae_lib ihierarchy imonad_lib