Theorem is_univalent_reindexing_forward_of_univalent (uD : is_univalent_disp D) (uC' : is_univalent C') (uC : is_univalent C) : is_univalent_disp D'. Proof. apply is_univalent_disp_from_fibers. intros c' x' y'. use weqhomot. - apply (weqcomp weq_reindexing_forward_ob_eq_Split_eq). apply (weqcomp (weq_Split_eq_Split_z_iso uC uC' uD)). exact weq_reindexing_forward_Split_z_iso_ob_z_iso. - intro e. destruct e. apply eq_z_iso_disp. cbn. apply maponpaths. apply two_arg_paths. * apply uip. apply homset_property. * reflexivity. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.NaturalTransformations. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.StreetFibration.