Definition z_iso_disp_mono_codomain {C : category} {x y : C} {f : z_iso x y} {h₁ : disp_mono_codomain C x} {h₂ : disp_mono_codomain C y} (g : z_iso (pr11 h₁) (pr11 h₂)) (p : g · pr21 h₂ = pr21 h₁ · f) : z_iso_disp f h₁ h₂. Proof. use make_z_iso_disp. - exact ((pr1 g ,, p) ,, tt). - simple refine ((_ ,, tt) ,, _ ,, _). + refine (inv_from_z_iso g ,, _). abstract (use z_iso_inv_on_right ; rewrite !assoc ; use z_iso_inv_on_left ; 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.