Definition iso_to_disp_iso_mono_cod (h : z_iso y z) (p : f = h · g) : z_iso_disp (identity_z_iso x) fy gz. Proof. use make_z_iso_disp. - refine ((pr1 h ,, _) ,, tt). abstract (cbn ; rewrite id_right ; exact (!p)). - simple refine ((_ ,, tt) ,, _ ,, _). + refine (inv_from_z_iso h ,, _). abstract (cbn ; rewrite id_right ; use z_iso_inv_on_right ; exact p). + 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.