proposition: Lemma morphism_class_retract_closed_impl_eq_cl {C : category} (S : morphism_class C) : morphism_class_retract_closed S -> S^cl = S.
proof: Proof. intro H. apply morphism_class_subset_antisymm. - intros x y f Hf. simpl in Hf. use (hinhuniv _ Hf). clear Hf; intro Hf; destruct Hf as [x' [y' [f' Hf']]]. apply (H _ _ f _ _ f' Hf'). - intros x y f Hf. apply in_morcls_retc_if_in_morcls. exact Hf. Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.opp_precat UniMath.ModelCategories.Retract