Lemma isantisymm_SubObj_rel (c : C) : isantisymm (SubObj_rel c). Proof. unfold isantisymm; simpl. assert (int : ∏ x1 x2, isaprop (SubObj_rel c x1 x2 → SubObj_rel c x2 x1 -> x1 = x2)). { intros x1 x2. repeat (apply impred; intro). apply (isasetsetquot _ x1 x2). } apply (setquotuniv2prop _ (λ x1 x2, make_hProp _ (int x1 x2))). intros x y h1 h2. simpl in *. apply (iscompsetquotpr (z_iso_eqrel (C:=Subobjectscategory c))). generalize h1; clear h1; apply hinhuniv; intros [h1 Hh1]. generalize h2; clear h2; apply hinhuniv; intros [h2 Hh2]. apply hinhpr, (invmap (weq_z_iso _ (subprecategory_of_monics_ob C c) _ _)). induction x as [[x []] [fx Hfx]]. induction y as [[y []] [fy Hfy]]. simpl in *. assert (mon_h1 : isMonic h1). { apply (isMonic_postcomp _ h1 fy); rewrite <- Hh1; apply Hfx. } assert (mon_h2 : isMonic h2). { apply (isMonic_postcomp _ h2 fx); rewrite <- Hh2; apply Hfy. } use tpair. - exists (h1,,mon_h1). exists (h2,,mon_h2). split; apply subtypePath. + intros xx. apply isapropisMonic. + simpl; apply Hfx. now rewrite <- assoc, <- Hh2, <- Hh1, id_left. + intros xx. apply isapropisMonic. + simpl; apply Hfy. now rewrite <- assoc, <- Hh1, <- Hh2, id_left. - apply subtypePath; simpl; try apply Hh1. now intros xx; apply isapropisMonic. Qed.
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.