proposition: Lemma morphism_class_retract_closed_iff_eq_cl {C : category} (S : morphism_class C) : morphism_class_retract_closed S <-> S^cl = S.
proof: Proof. split. - exact (morphism_class_retract_closed_impl_eq_cl S). - exact (morphism_class_retract_closed_if_eq_cl S). Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.opp_precat UniMath.ModelCategories.Retract