Definition from_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} (ff : z_iso_disp f h₁ h₂) : z_iso (pr11 h₁) (pr11 h₂). Proof. use make_z_iso. - exact (pr111 ff). - exact (pr1 (pr112 ff)). - split. + abstract (refine (maponpaths (λ z, pr11 z) (pr222 ff) @ _) ; rewrite transportb_mono_cod_disp ; apply idpath). + abstract (refine (maponpaths (λ z, pr11 z) (pr122 ff) @ _) ; rewrite transportb_mono_cod_disp ; apply idpath). 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.