Definition univ_prop_reindexing_forward : disp_nat_z_iso (DF ◦ DH) DG (nat_z_iso_id (F ∙ H)). Proof. - repeat use tpair. * exact (λ c d,id_disp (DG c d)). * intros a b f x y Df. cbn. etrans. apply id_right_disp. apply pathsinv0. rewrite id_left_disp. etrans. apply transport_b_b. apply two_arg_paths. -- apply uip. apply homset_property. -- reflexivity. * intros c d. cbn. exists (id_disp (DG c d)). split; apply id_left_disp. 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.