proposition: Lemma morphism_class_retract_closed_if_eq_cl {C : category} (S : morphism_class C) : S^cl = S -> morphism_class_retract_closed S.
proof: Proof. intro H. intros x y f x' y' f' Hf'. rewrite <- H. apply hinhpr. exists _, _, f'. exact Hf'. Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.opp_precat UniMath.ModelCategories.Retract