Lemma univalent_disp_cat_has_groupoid_obs {C} (D : disp_cat C) (is_u : is_univalent_disp D) : ∏ c, isofhlevel 3 (D c). 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.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos.