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. 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.
Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Categories.HSET.MonoEpiIso. Require Import UniMath.CategoryTheory.Categories.HSET.Univalence. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.Presheaf. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.NaturalTransformations. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Examples.Opposite. Section IsoCleavingFromOpcleaving. End IsoCleavingFromOpcleaving.