proposition: Lemma isasetmorphism_class {C : category} : isaset (morphism_class C).
proof: Proof. change (isaset) with (isofhlevel 2). apply impred; intro x. apply impred; intro t. exact (isasethsubtype _). Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.opp_precat UniMath.ModelCategories.Retract