proposition: Lemma ToBinDirectSumFormulaUnique {a b : A} (B : BinDirectSum a b) {c : A} (f : c --> a) (g : c --> b) : ToBinDirectSumFormula B f g = ToBinDirectSum B f g.
proof: Proof. apply ToBinDirectSumUnique. - unfold ToBinDirectSumFormula. unfold to_binop. use (pathscomp0 (to_postmor_linear c (to_Pr1 B) (f · to_In1 B) (g · to_In2 B))). unfold to_postmor. repeat rewrite <- assoc. rewrite (to_IdIn1 B). rewrite id_right. rewrite (to_Unel2 B). set (XX := to_premor_unel A a g). unfold to_premor in XX. unfold to_unel. rewrite XX. apply (to_runax c a). - unfold ToBinDirectSumFormula. unfold to_binop. cbn. use (pathscomp0 (to_postmor_linear c (to_Pr2 B) (f · to_In1 B) (g · to_In2 B))). unfold to_postmor. repeat rewrite <- assoc. rewrite (to_IdIn2 B). rewrite (to_Unel1 B). rewrite id_right. set (XX := to_premor_unel A b f). unfold PrecategoriesWithAbgrops.to_premor in XX. unfold PrecategoriesWithAbgrops.to_unel. rewrite XX. clear XX. apply (to_lunax c b). 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