proposition: Theorem is_cleaving_reindexing_forward_of_cleaving (cl:cleaving D) (st: street_fib F) (univ : is_univalent C') : cleaving D'.
proof: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.NaturalTransformations UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.DisplayedCats.Univalence UniMath.CategoryTheory.DisplayedCats.Fibrations UniMath.CategoryTheory.DisplayedCats.StreetFibration