proposition: Lemma FromBinDirectSumFormulaUnique {a b : A} (B : BinDirectSum a b) {c : A} (f : a --> c) (g : b --> c) : FromBinDirectSumFormula B f g = FromBinDirectSum B f g.
proof: Proof. unfold FromBinDirectSumFormula. apply FromBinDirectSumUnique. - use (pathscomp0 (to_premor_linear c (to_In1 B) (to_Pr1 B · f) (to_Pr2 B · g))). unfold to_premor. repeat rewrite assoc. rewrite (to_IdIn1 B). rewrite (to_Unel1 B). rewrite id_left. set (XX := to_postmor_unel A a g). unfold to_postmor in XX. unfold to_unel. rewrite XX. apply (to_runax a c). - use (pathscomp0 (to_premor_linear c (to_In2 B) (to_Pr1 B · f) (to_Pr2 B · g))). unfold to_premor. repeat rewrite assoc. rewrite (to_IdIn2 B). rewrite (to_Unel2 B). rewrite id_left. set (XX := to_postmor_unel A b f). unfold to_postmor in XX. unfold to_unel. rewrite XX. apply (to_lunax b c). 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