proposition: Lemma univalent_disp_cat_has_groupoid_obs {C} (D : disp_cat C) (is_u : is_univalent_disp D) : ∏ c, isofhlevel 3 (D c).
proof: Proof. intro c. change (isofhlevel 3 (D c)) with (∏ a b : D c, isofhlevel 2 (a = b)). intros xx xx'. set (XR := is_univalent_in_fibers_from_univalent_disp _ is_u). apply (isofhlevelweqb _ (make_weq _ (XR _ xx xx'))). apply isaset_z_iso_disp. Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.PartA UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Isos