Definition disp_iso_weq_iso_mono_cod : (∑ (h : z_iso y z), f = h · g) ≃ z_iso_disp (identity_z_iso x) fy gz. Proof. use weq_iso. - exact (λ h, iso_to_disp_iso_mono_cod (pr1 h) (pr2 h)). - exact disp_iso_to_iso_mono_cod. - abstract (intro ff ; use subtypePath ; [ intro ; apply homset_property | ] ; use z_iso_eq ; cbn ; apply idpath). - abstract (intro ff ; use subtypePath ; [ intro ; apply isaprop_is_z_iso_disp | ] ; apply locally_propositional_mono_cod_disp_cat). 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.