fact: Definition morphism_class_retract_closed {C : category} (S : morphism_class C) : UU := ∏ x y (f : x --> y) x' y' (f' : x' --> y'), (S _ _ f') × (retract f' f) -> (S _ _ f).
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.opp_precat UniMath.ModelCategories.Retract