Definition disp_iso_to_iso (ff : z_iso_disp (identity_z_iso x) fy gz) : ∑ (h : z_iso y z), f = h · g. Proof. simple refine (_ ,, _). - use make_z_iso. + exact (pr11 ff). + exact (pr1 (inv_mor_disp_from_z_iso ff)). + split. * abstract (refine (maponpaths pr1 (inv_mor_after_z_iso_disp ff) @ _) ; rewrite transportb_cod_disp ; apply idpath). * abstract (refine (maponpaths pr1 (z_iso_disp_after_inv_mor ff) @ _) ; rewrite transportb_cod_disp ; apply idpath). - abstract (refine (!(pr21 ff @ _)) ; apply id_right). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations.