Lemma isaset_setcategory_total_morphisms (C : setcategory): isaset (total_morphisms C). 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.
Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.Sets. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Setcategories.