fact: Definition BinDirectSum (a b : A) : UU := ∑ coab : (∑ co : A, a --> co × b --> co × co --> a × co --> b), isBinDirectSum a b (pr1 coab) (pr1 (pr2 coab)) (pr1 (pr2 (pr2 coab))) (pr1 (pr2 (pr2 (pr2 coab)))) (pr2 (pr2 (pr2 (pr2 coab)))).
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