proposition: 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: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.DisplayedCats.Codomain UniMath.CategoryTheory.DisplayedCats.Fibrations