Definition is_z_iso_disp_mono_codomain {C : category} {x : C} {fy gz : disp_mono_codomain C x} (φp : fy -->[ identity x ] gz) (H : is_z_isomorphism (pr11 φp)) : is_z_iso_disp (identity_z_iso x) φp. Proof. pose (h := (_ ,, H) : z_iso _ _). simple refine ((_ ,, tt) ,, _ ,, _). - refine (inv_from_z_iso h ,, _). abstract (cbn ; use z_iso_inv_on_right ; rewrite id_right ; refine (_ @ !(pr21 φp)) ; rewrite id_right ; apply idpath). - apply locally_propositional_mono_cod_disp_cat. - 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.