Definition SubObj_rel (c : C) : hrel (pr1 (SubObj c)). Proof. use quotrel. - apply monorel. - intros x1 y1 x2 y2 h1 h2. apply hPropUnivalence. + apply (are_z_isomorphic_monorel h1 h2). + apply (are_z_isomorphic_monorel (eqrelsymm (z_iso_eqrel) _ _ h1) (eqrelsymm (z_iso_eqrel) _ _ h2)). Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.slicecat. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.Subcategory.Core. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.opp_precat.