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. 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.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.Algebra.BinaryOperations. Require Import UniMath.Algebra.Groups. Require Import UniMath.Algebra.Monoids. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Zero. Require Import UniMath.CategoryTheory.CategoriesWithBinOps. Require Import UniMath.CategoryTheory.PrecategoriesWithAbgrops. Require Import UniMath.CategoryTheory.PreAdditive. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.Epis. Definition FromBinDirectSum {a b : A} (B : BinDirectSum a b) {c : A} (f : a --> c) ∏ (c : A) (f : a --> c) (g : b --> c), (to_In1 B) · (FromBinDirectSum B f g) = f. ∏ (c : A) (f : a --> c) (g : b --> c), (to_In2 B) · (FromBinDirectSum B f g) = g. Definition FromBinDirectSumUnique {a b : A} (B : BinDirectSum a b) {c : A} (f : a --> c) to_In1 B · k = f -> to_In2 B · k = g -> k = FromBinDirectSum B f g := Lemma FromBinDirectSumsEq {c d : A} (DS : BinDirectSum c d) {x : A} (k1 k2 : DS --> x) : rewrite (FromBinDirectSumUnique DS (to_In1 DS · k1) (to_In2 DS · k1) k1). apply FromBinDirectSumUnique. Definition FromBinDirectSumFormula {a b : A} (B : BinDirectSum a b) {c : A} (f : a --> c) 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. unfold FromBinDirectSumFormula. apply FromBinDirectSumUnique. A⟦B1, B2⟧ := FromBinDirectSum B1 (f · (to_In1 B2)) (g · (to_In2 B2)). rewrite <- FromBinDirectSumFormulaUnique. unfold FromBinDirectSumFormula. + exact (to_quot_mor A PAS (FromBinDirectSum A (BD x y) f1 g1)). rewrite <- (@id_left A _ _ (FromBinDirectSum A (BD x y) f1 g1)). - apply ArrowsFromZero. - apply ArrowsFromZero.