proposition: Proposition is_univalent_disp_indexed_cat_to_disp_cat : is_univalent_disp indexed_cat_to_disp_cat.
proof: Proof. use is_univalent_disp_from_fibers. intros x xx₁ xx₂. use weqhomot. - exact (indexed_cat_to_disp_cat_z_iso_weq xx₁ xx₂ ∘ make_weq idtoiso (pr2 (Φ x) _ _))%weq. - abstract (intro p ; induction p ; use subtypePath ; [ intro ; apply isaprop_is_z_iso_disp | ] ; cbn ; apply id_left). Defined.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.OppositeCategory.Core UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.DisplayedCats.Fibrations UniMath.CategoryTheory.DisplayedCats.Fiber UniMath.CategoryTheory.DisplayedCats.Univalence UniMath.CategoryTheory.IndexedCategories.IndexedCategory