Proposition eq_subobject_univ_cat {y₁ y₂ : mono_in_cat x} (f : z_iso y₁ y₂) (p : f · monic_of_mono_in_cat y₂ = monic_of_mono_in_cat y₁) : y₁ = y₂. Proof. use (isotoid_disp (univalent_disp_mono_codomain C) (idpath _)). use z_iso_disp_mono_codomain. - exact f. - cbn. rewrite id_right. exact p. Qed.
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.