proposition: Lemma Quotcategory_isBinCoproduct (x y : A) : isBinCoproduct (Quotcategory_PreAdditive A PAS PAC) x y (BD x y) (to_quot_mor A PAS (to_In1 (BD x y))) (to_quot_mor A PAS (to_In2 (BD x y))).
proof: Proof. use make_isBinCoproduct. - apply has_homsets_Quotcategory. - intros c f g. set (f'' := @issurjsetquotpr (@to_abgr A x c) (binopeqrel_subgr_eqrel (PAS x c)) f). use (squash_to_prop f''). apply isapropiscontr. intros f'. clear f''. set (g'' := @issurjsetquotpr (@to_abgr A y c) (binopeqrel_subgr_eqrel (PAS y c)) g). use (squash_to_prop g''). apply isapropiscontr. intros g'. clear g''. induction f' as [f1 f2]. induction g' as [g1 g2]. cbn in f1, g1. use unique_exists. + exact (to_quot_mor A PAS (FromBinDirectSum A (BD x y) f1 g1)). + cbn beta. split. * use (pathscomp0 (Quotcategory_comp_linear A PAS PAC _ _)). rewrite BinDirectSumIn1Commutes. exact f2. * use (pathscomp0 (Quotcategory_comp_linear A PAS PAC _ _)). rewrite BinDirectSumIn2Commutes. exact g2. + intros y0. apply isapropdirprod; apply has_homsets_Quotcategory. + intros y0 T. cbn beta in T. induction T as [T1 T2]. * set (y'' := @issurjsetquotpr (@to_abgr A (BD x y) c) (binopeqrel_subgr_eqrel (PAS (BD x y) c)) y0). use (squash_to_prop y''). apply has_homsets_Quotcategory. intros y'. clear y''. induction y' as [y1 y2]. rewrite <- y2. rewrite <- y2 in T1. rewrite <- y2 in T2. cbn in y1. rewrite <- (@id_left (Quotcategory_PreAdditive A PAS PAC) _ _ (setquotpr (binopeqrel_subgr_eqrel (PAS (BD x y) c)) y1)). rewrite <- (@id_left A _ _ (FromBinDirectSum A (BD x y) f1 g1)). rewrite <- (to_BinOpId (BD x y)). rewrite to_postmor_linear'. repeat rewrite <- assoc. rewrite BinDirectSumIn1Commutes. rewrite BinDirectSumIn2Commutes. rewrite <- f2 in T1. rewrite <- g2 in T2. unfold to_quot_mor. set (tmp := @setquotpr_linear A PAS PAC (BD x y) c). unfold to_quot_mor in tmp. rewrite tmp. clear tmp. set (tmp := @Quotcategory_comp_linear A PAS PAC (BD x y) x c). unfold to_quot_mor in tmp. rewrite <- tmp. clear tmp. rewrite <- T1. set (tmp := @Quotcategory_comp_linear A PAS PAC (BD x y) y c). unfold to_quot_mor in tmp. rewrite <- tmp. clear tmp. rewrite <- T2. unfold to_quot_mor. rewrite comp_eq. rewrite comp_eq. rewrite assoc. rewrite assoc. rewrite <- to_postmor_linear'. repeat rewrite <- comp_eq. set (tmp := @Quotcategory_comp_linear A PAS PAC (BD x y) x (BD x y)). unfold to_quot_mor in tmp. rewrite tmp. clear tmp. set (tmp := @Quotcategory_comp_linear A PAS PAC (BD x y) y (BD x y)). unfold to_quot_mor in tmp. rewrite tmp. clear tmp. set (tmp := @setquotpr_linear A PAS PAC (BD x y) (BD x y)). unfold to_quot_mor in tmp. rewrite <- tmp. clear tmp. rewrite comp_eq. rewrite (to_BinOpId (BD x y)). rewrite comp_eq. apply cancel_postcomposition. apply idpath. Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Notations UniMath.Algebra.BinaryOperations UniMath.Algebra.Groups UniMath.Algebra.Monoids UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Zero UniMath.CategoryTheory.CategoriesWithBinOps UniMath.CategoryTheory.PrecategoriesWithAbgrops UniMath.CategoryTheory.PreAdditive UniMath.CategoryTheory.Monics UniMath.CategoryTheory.Epis