Definition z_iso_is_cartesian_sfib {C₁ C₂ : category} (F : C₁ ⟶ C₂) {x₁ x₂ : C₁} (i : x₁ --> x₂) (Hi : is_z_isomorphism i) : is_cartesian_sfib F i. Proof. pose (i_iso := make_z_iso' _ Hi). intros w g h p. use iscontraprop1. - abstract (use invproofirrelevance ; intros φ₁ φ₂ ; use subtypePath ; [ intro ; apply isapropdirprod ; apply homset_property | ] ; refine (!(id_right _) @ _ @ id_right _) ; rewrite <- (z_iso_inv_after_z_iso i_iso) ; cbn ; rewrite !assoc ; rewrite (pr22 φ₁), (pr22 φ₂) ; apply idpath). - simple refine (_ ,, _ ,, _). + exact (g · inv_from_z_iso i_iso). + abstract (rewrite functor_comp ; rewrite p ; rewrite !assoc' ; rewrite <- functor_comp ; etrans ; [ do 2 apply maponpaths ; exact (z_iso_inv_after_z_iso i_iso) | ] ; rewrite functor_id ; apply id_right). + abstract (cbn ; rewrite !assoc' ; refine (_ @ id_right _) ; apply maponpaths ; apply z_iso_after_z_iso_inv). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations.