fact: Definition make_isBinDirectSum (a b co : A) (i1 : a --> co) (i2 : b --> co) (p1 : co --> a) (p2 : co --> b) (H1 : i1 · p1 = identity a) (H2 : i2 · p2 = identity b) (H3 : i1 · p2 = (to_unel a b)) (H4 : i2 · p1 = (to_unel b a)) (H5 : (to_binop co co) (p1 · i1) (p2 · i2) = identity co) : isBinDirectSum a b co i1 i2 p1 p2 := H1,,H2,,H3,,H4,,H5.
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