proposition: Lemma joinretM : hierarchy.JoinLaws.left_unit ret join.
proof: Proof. by move=> a; apply funext=> x; rewrite joinE retE (category.joinretM a). Qed.
imports: mathcomp(all_ssreflect) mathcomp(boolp) monae_lib HB(structures) hierarchy