Definition z_iso_fiber_from_z_iso_disp (a b : fiber_category) : z_iso a b <- z_iso_disp (identity_z_iso c) a b. Proof. intro i. use tpair. + apply (pr1 i). + cbn in *. use tpair. apply (inv_mor_disp_from_z_iso i). abstract (split; cbn; [ assert (XR := inv_mor_after_z_iso_disp i); etrans; [ apply maponpaths , XR |]; etrans; [ apply transport_f_f |]; apply transportf_comp_lemma_hset; try apply homset_property; apply idpath | assert (XR := z_iso_disp_after_inv_mor i); etrans; [ apply maponpaths , XR |] ; etrans; [ apply transport_f_f |]; apply transportf_comp_lemma_hset; try apply homset_property; apply idpath ]). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.NaturalTransformations. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Total.