Definition z_iso_disp_from_z_iso_fiber (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. use tpair. * apply (inv_from_z_iso i). * abstract ( split; [ assert (XR := z_iso_after_z_iso_inv i); cbn in *; assert (XR' := transportf_pathsinv0' _ _ _ _ XR); etrans; [ apply (!XR') |]; unfold transportb; apply maponpaths_2; apply homset_property |assert (XR := z_iso_inv_after_z_iso i); cbn in *; assert (XR' := transportf_pathsinv0' _ _ _ _ XR); etrans; [ apply (!XR') | ]; unfold transportb; apply maponpaths_2; apply homset_property ] ). 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.