Definition is_z_iso_disp_cartesian_factorisation {C : category} {D : disp_cat C} {w x y : C} {f : w --> x} (Hf : is_z_isomorphism f) (fiso := (f ,, Hf) : z_iso w x) {g : x --> y} (Hg : is_z_isomorphism g) (giso := (g ,, Hg) : z_iso x y) {ww : D w} {xx : D x} {yy : D y} {gg : xx -->[ g ] yy} (Hgg : is_cartesian gg) (hh : ww -->[ f · g ] yy) (Hhh : is_z_iso_disp (z_iso_comp fiso giso) hh) : is_z_iso_disp fiso (cartesian_factorisation Hgg f hh). Proof. simple refine (_ ,, _ ,, _). - refine (transportf (λ z, _ -->[ z ] _) _ (gg ;; inv_mor_disp_from_z_iso Hhh)%mor_disp). abstract (cbn ; rewrite !assoc ; refine (_ @ id_left _) ; apply maponpaths_2 ; exact (z_iso_inv_after_z_iso giso)). - use (cartesian_factorisation_unique Hgg). rewrite mor_disp_transportf_postwhisker. rewrite assoc_disp_var. rewrite !mor_disp_transportf_postwhisker. rewrite assoc_disp_var. rewrite !transport_f_f. rewrite assoc_disp_var. rewrite !mor_disp_transportf_prewhisker. rewrite transport_f_f. rewrite cartesian_factorisation_commutes. etrans ; [ do 2 apply maponpaths ; apply (z_iso_disp_after_inv_mor Hhh) | ]. unfold transportb. rewrite mor_disp_transportf_prewhisker. rewrite transport_f_f. rewrite id_right_disp. rewrite mor_disp_transportf_postwhisker. rewrite id_left_disp. unfold transportb. rewrite !transport_f_f. apply maponpaths_2. apply homset_property. - cbn. rewrite mor_disp_transportf_prewhisker. rewrite assoc_disp. unfold transportb. rewrite transport_f_f. rewrite cartesian_factorisation_commutes. refine (maponpaths _ (inv_mor_after_z_iso_disp Hhh) @ _). unfold transportb. rewrite transport_f_f. apply maponpaths_2. apply 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.