proposition: Lemma total_category_has_homsets {C : category} (D : disp_cat C) : has_homsets (total_category_data D).
proof: Proof. intros ? ?; simpl. apply isaset_total2. apply homset_property. intros; apply homsets_disp. Qed.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.AxiomOfChoice UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.NaturalTransformations UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.DisplayedCats.Univalence