Definition is_univalent_reindex_disp_cat {C₁ C₂ : category} (F : C₁ ⟶ C₂) (D : disp_cat C₂) (HD : is_univalent_disp D) : is_univalent_disp (reindex_disp_cat F D). Proof. intros x y p xx yy. induction p. use weqhomot. - exact (z_iso_disp_weq_z_iso_disp_reindex xx yy ∘ make_weq (@idtoiso_disp _ D _ _ (idpath _) xx yy) (HD _ _ _ xx yy))%weq. - abstract (intros p ; induction p ; use subtypePath ; [ intro ; apply isaprop_is_z_iso_disp | ] ; apply idpath). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.NaturalTransformations. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Section IsCartesianFromReindexDispCat. End IsCartesianFromReindexDispCat. Section IsOpCartesianFromReindexDispCat. End IsOpCartesianFromReindexDispCat.