Lemma is_cartesian_from_z_iso_to_cartesian {C : category} {D : disp_cat C} {c} {d : D c} {c' : C} {f : c' --> c} {d0'} {ff : d0' -->[f] d} (ff_cart : is_cartesian ff) {d1'} {ff' : d1' -->[f] d} (i : z_iso_disp (identity_z_iso _) d0' d1') (e : (i ;; ff')%mor_disp = transportb _ (id_left _) ff) : is_cartesian ff'. Proof. intros c'' g d'' h. refine (iscontrweqf _ (ff_cart c'' g d'' h)). use weq_subtypes'. - eapply weqcomp. + exists (fun gg => (gg ;; i))%mor_disp. apply z_iso_disp_postcomp. + exists (transportf _ (id_right _)). apply isweqtransportf. - intro; apply homsets_disp. - intro; apply homsets_disp. - simpl. intros gg. assert (forall X (x y z : X), x = y -> (x = z <-> y = z)) as H. { intros X x y z p; split. + intros q; exact (!p @ q). + intros q; exact (p @ q). } apply H. apply pathsinv0. etrans. apply mor_disp_transportf_postwhisker. etrans. eapply transportf_bind. apply assoc_disp_var. etrans. eapply transportf_bind. etrans. apply maponpaths, e. apply mor_disp_transportf_prewhisker. refine (_ @ idpath_transportf _ _). apply maponpaths_2, homset_property. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations.