proposition: Lemma isaset_setcategory_total_morphisms (C : setcategory): isaset (total_morphisms C).
proof: Proof. change isaset with (isofhlevel 2). apply isofhleveltotal2. apply isofhleveldirprod. - exact (pr1 (pr2 C)). - exact (pr1 (pr2 C)). - intro ab; apply ((pr2 (pr2 C)) (dirprod_pr1 ab) (dirprod_pr2 ab)). Qed.
imports: UniMath.Foundations.PartA UniMath.Foundations.Sets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Setcategories