Definition z_iso_disp_to_is_cartesian {C : category} {D : disp_cat C} {x y z : C} {f : x --> z} {g : y --> z} {h : y --> x} (Hh : is_z_isomorphism h) {p : h · f = g} {xx : D x} {yy : D y} {zz : D z} {ff : xx -->[ f ] zz} {gg : yy -->[ g ] zz} {hh : yy -->[ h ] xx} (Hff : is_cartesian ff) (Hhh : is_z_iso_disp (make_z_iso' h Hh) hh) (pp : (hh ;; ff = transportb _ p gg)%mor_disp) : is_cartesian gg. Proof. intros q k qq kg. assert (f = inv_from_z_iso (make_z_iso' h Hh) · g) as r. { abstract (refine (!_) ; use z_iso_inv_on_right ; exact (!p)). } assert (transportf (λ z, _ -->[ z ] _) r ff = inv_mor_disp_from_z_iso Hhh ;; gg)%mor_disp as rr. { abstract (rewrite <- (transportb_transpose_left pp) ; unfold transportb ; rewrite mor_disp_transportf_prewhisker ; rewrite assoc_disp ; refine (!_) ; etrans ; [ do 2 apply maponpaths ; apply maponpaths_2 ; exact (z_iso_disp_after_inv_mor Hhh) | ] ; unfold transportb ; rewrite mor_disp_transportf_postwhisker ; rewrite id_left_disp ; unfold transportb ; rewrite !transport_f_f ; apply maponpaths_2 ; apply homset_property). } use iscontraprop1. - abstract (use invproofirrelevance ; intros φ₁ φ₂ ; use subtypePath ; [ intro ; apply D | ] ; use (postcomp_with_z_iso_disp_is_inj Hh (idpath _) Hhh) ; cbn ; use (cartesian_factorisation_unique Hff) ; rewrite !assoc_disp_var ; rewrite pp ; unfold transportb ; rewrite !mor_disp_transportf_prewhisker ; rewrite !transport_f_f ; apply maponpaths ; exact (pr2 φ₁ @ !(pr2 φ₂))). - simple refine (_ ,, _). + refine (transportf (λ z, _ -->[ z ] _) _ (cartesian_factorisation Hff (k · h) (transportf (λ z, _ -->[ z ] _) _ kg) ;; inv_mor_disp_from_z_iso Hhh)%mor_disp). * abstract (rewrite assoc' ; etrans ; [ apply maponpaths ; apply (z_iso_inv_after_z_iso (make_z_iso' h Hh)) | ] ; apply id_right). * abstract (rewrite assoc' ; rewrite p ; apply idpath). + abstract (simpl ; rewrite mor_disp_transportf_postwhisker ; rewrite assoc_disp_var ; etrans ; [ do 3 apply maponpaths ; exact (!rr) | ] ; rewrite transport_f_f ; rewrite mor_disp_transportf_prewhisker ; rewrite cartesian_factorisation_commutes ; rewrite !transport_f_f ; apply transportf_set ; 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.