Definition disp_iso_to_iso_mono_cod (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 (pr111 ff). + exact (pr11 (inv_mor_disp_from_z_iso ff)). + split. * abstract (refine (maponpaths (λ z, pr11 z) (inv_mor_after_z_iso_disp ff) @ _) ; rewrite transportb_mono_cod_disp ; apply idpath). * abstract (refine (maponpaths (λ z, pr11 z) (z_iso_disp_after_inv_mor ff) @ _) ; rewrite transportb_mono_cod_disp ; apply idpath). - abstract (refine (!(pr211 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.Monics. 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. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.CategoryTheory.DisplayedCats.Examples.Sigma.