proposition: Lemma morphism_class_ext {C : category} {I J : morphism_class C} (h : ∏ x y (f : x --> y), ((I _ _) f <-> (J _ _) f)) : I = J.
proof: Proof. do 3 (apply funextsec; intro). destruct ((h x x0 x1)) as [impl conv]. exact (hPropUnivalence _ _ impl conv). Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.opp_precat UniMath.ModelCategories.Retract