Proposition is_univalent_disp_indexed_cat_to_disp_cat : is_univalent_disp indexed_cat_to_disp_cat. 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.
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.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.OppositeCategory.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.IndexedCategories.IndexedCategory.