Theorem is_cleaving_reindexing_forward_of_cleaving (cl:cleaving D) (st: street_fib F) (univ : is_univalent C') : cleaving D'. Proof. intros b' a' f' y'. set (st_fib := st ↙y' a' (transportb _ ¤y' f')). set (a := pr1 st_fib). set (f := pr112 st_fib : C ⟦ a, ↙y' ⟧). set (px := isotoid C' univ (pr212 st_fib) : F a = a'). set (cl_fib := cl ↙y' a f ←y'). set (x := pr1 cl_fib). set (ff := pr12 cl_fib : x -->[f] ←y'). assert (double_transport px ¤y' (# F f) = f') as pf. { unfold double_transport. apply transportf_transpose_left. etrans. apply transportf_isotoid. apply z_iso_inv_on_right. exact (pr122 st_fib). } set (x' := (a,, px,, x) : D' a'). set (ff' := (f,, pf,, ff) : x' -->[f'] y'). exists x'. exists ff'. apply (is_cartesian_reindexing_forward_of_cleaving ff' (pr222 st_fib) cl_fib). 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.