proposition: Lemma Quotcategory_isBinDirectSum (x y : A) : isBinDirectSum (A := Quotcategory_PreAdditive A PAS PAC) (to_quot_mor A PAS (to_In1 (BD x y))) (to_quot_mor A PAS (to_In2 (BD x y))) (to_quot_mor A PAS (to_Pr1 (BD x y))) (to_quot_mor A PAS (to_Pr2 (BD x y))).
proof: Proof. use make_isBinDirectSum. - unfold to_quot_mor. rewrite <- comp_eq. set (tmp := @Quotcategory_comp_linear A PAS PAC x (BD x y) x). unfold to_quot_mor in tmp. rewrite tmp. clear tmp. rewrite (to_IdIn1 (BD x y)). apply idpath. - unfold to_quot_mor. rewrite <- comp_eq. set (tmp := @Quotcategory_comp_linear A PAS PAC y (BD x y) y). unfold to_quot_mor in tmp. rewrite tmp. clear tmp. rewrite (to_IdIn2 (BD x y)). apply idpath. - unfold to_quot_mor. rewrite <- comp_eq. set (tmp := @Quotcategory_comp_linear A PAS PAC x (BD x y) y). unfold to_quot_mor in tmp. rewrite tmp. clear tmp. rewrite (to_Unel1 (BD x y)). apply idpath. - unfold to_quot_mor. rewrite <- comp_eq. set (tmp := @Quotcategory_comp_linear A PAS PAC y (BD x y) x). unfold to_quot_mor in tmp. rewrite tmp. clear tmp. rewrite (to_Unel2 (BD x y)). apply idpath. - unfold to_quot_mor. 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 (to_BinOpId (BD x y)). 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