Definition is_cartesian_z_iso_disp {C : category} {D : disp_cat C} {x : C} {xx : D x} {y : C} {yy : D y} {f : x --> y} {Hf : is_z_isomorphism f} {ff : xx -->[ f ] yy} (Hff : is_z_iso_disp (make_z_iso' f Hf) ff) : is_cartesian ff. Proof. intros z g zz gf. use iscontraprop1. - abstract (apply invproofirrelevance ; intros φ₁ φ₂ ; use subtypePath ; [ intro ; apply D | ] ; pose (pr2 φ₁ @ !(pr2 φ₂)) as r ; refine (id_right_disp_var _ @ _ @ !(id_right_disp_var _)) ; pose (transportf_transpose_left (inv_mor_after_z_iso_disp Hff)) as r' ; rewrite <- !r' ; clear r' ; rewrite !mor_disp_transportf_prewhisker ; rewrite !assoc_disp ; unfold transportb ; rewrite !transport_f_f ; apply maponpaths ; apply maponpaths_2 ; exact r). - simple refine (_ ,, _). + refine (transportf (λ z, _ -->[ z ] _) _ (gf ;; inv_mor_disp_from_z_iso Hff)%mor_disp). abstract (rewrite assoc' ; refine (_ @ id_right _) ; apply maponpaths ; apply (z_iso_inv_after_z_iso (make_z_iso' f Hf))). + abstract (simpl ; rewrite mor_disp_transportf_postwhisker ; rewrite assoc_disp_var ; rewrite transport_f_f ; etrans ; [ do 2 apply maponpaths ; apply (z_iso_disp_after_inv_mor Hff) | ] ; unfold transportb ; rewrite mor_disp_transportf_prewhisker ; rewrite transport_f_f ; rewrite id_right_disp ; unfold transportb ; rewrite transport_f_f ; apply transportf_set ; apply homset_property ; rewrite disp_id_right). 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.