proposition: Lemma is_z_iso_from_is_cartesian {C : category} {D : disp_cat C} {c c' : C} (i : z_iso c' c) {d : D c} {d'} (ff : d' -->[i] d) : is_cartesian ff -> is_z_iso_disp i ff.
proof: Proof. intros Hff. use (_,,_); try split. - use (cartesian_factorisation' Hff (inv_from_z_iso i) (id_disp _)). apply z_iso_after_z_iso_inv. - apply cartesian_factorisation_commutes'. - apply (cartesian_factorisation_unique Hff). etrans. apply assoc_disp_var. rewrite cartesian_factorisation_commutes'. etrans. eapply transportf_bind. etrans. apply mor_disp_transportf_prewhisker. eapply transportf_bind, id_right_disp. apply pathsinv0. etrans. apply mor_disp_transportf_postwhisker. etrans. eapply transportf_bind, id_left_disp. apply maponpaths_2, homset_property. Qed.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Categories.HSET.MonoEpiIso UniMath.CategoryTheory.Categories.HSET.Univalence UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Equivalences.Core UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.Presheaf UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.NaturalTransformations UniMath.CategoryTheory.DisplayedCats.Fiber UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.DisplayedCats.Univalence UniMath.CategoryTheory.DisplayedCats.Examples.Opposite