Definition cartesian_lifts_iso {C : category} {D : disp_cat C} {c} {d : D c} {c' : C} {f : c' --> c} (fd fd' : cartesian_lift d f) : z_iso_disp (identity_z_iso c') fd fd'. Proof. use (_,,(_,,_)). - exact (cartesian_factorisation' fd' (identity _) fd (id_left _)). - exact (cartesian_factorisation' fd (identity _) fd' (id_left _)). - cbn; split. + apply (cartesian_factorisation_unique fd'). etrans. apply assoc_disp_var. rewrite cartesian_factorisation_commutes'. etrans. eapply transportf_bind, mor_disp_transportf_prewhisker. rewrite cartesian_factorisation_commutes'. etrans. apply transport_f_f. apply pathsinv0. etrans. apply mor_disp_transportf_postwhisker. rewrite id_left_disp. etrans. apply transport_f_f. apply maponpaths_2, homset_property. + apply (cartesian_factorisation_unique fd). etrans. apply assoc_disp_var. rewrite cartesian_factorisation_commutes'. etrans. eapply transportf_bind, mor_disp_transportf_prewhisker. rewrite cartesian_factorisation_commutes'. etrans. apply transport_f_f. apply pathsinv0. etrans. apply mor_disp_transportf_postwhisker. rewrite id_left_disp. etrans. apply transport_f_f. apply maponpaths_2, homset_property. Defined.
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.