Lemma is_cartesian_reindexing_forward_of_cleaving {a' b' : C'} {f' : a' --> b'} {x' : D' a'} {y' : D' b'} (ff' : x' -->[f'] y') (st_car : is_cartesian_sfib F (↙ff')) (car : is_cartesian (←ff')) : is_cartesian ff'. Proof. intros c' g' z' hh'. set (Hyp1 := st_car (↙z') (↙hh') (double_transport (!¤z') (!¤x') g') (commute_in_C' ff' hh')). set (Hyp2 := car (↙z') (pr11 Hyp1) (←z') (transportb (mor_disp _ _) (pr221 Hyp1) (←hh'))). set (g:= pr11 Hyp1). set (pg := double_transport_transpose' (pr121 Hyp1)). set (gg := pr11 Hyp2). set (gg' := (g,, pg,, gg) : z' -->[ g'] x'). apply (unique_exists gg' (commute_in_D' ff' hh' (pr1 Hyp1) (pr1 Hyp2))). intro gg'_bis. - apply homsets_disp. - exact (unicity_gg' ff' gg' hh' (pr221 Hyp1) (λ g0, uniqueExists (b:= g0) Hyp1 (pr21 Hyp1)) (λ gg0, uniqueExists (b:= gg0) Hyp2 (pr21 Hyp2))). 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.