proposition: Lemma in_morcls_retc_if_in_morcls {C : category} (S : morphism_class C) {a b} (f : a --> b) : (S _ _ f) -> (S^cl _ _ f).
proof: Proof. intro H. apply hinhpr. exists _, _, f. exact (make_dirprod H (retract_self f)). Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.opp_precat UniMath.ModelCategories.Retract