proposition: Lemma isaprop_morphism_class_retract_closed {C : category} (S : morphism_class C) : isaprop (morphism_class_retract_closed S).
proof: Proof. do 7 (apply impred; intro). apply propproperty. Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.opp_precat UniMath.ModelCategories.Retract