proposition: Lemma isantisymm_SubObj_rel (c : C) : isantisymm (SubObj_rel c).
proof: 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.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.slicecat UniMath.CategoryTheory.Monics UniMath.CategoryTheory.Subcategory.Core UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.opp_precat