Lemma ToBinDirectSumsEq {c d : A} (DS : BinDirectSum c d) {x : A} (k1 k2 : x --> DS) : k1 · to_Pr1 DS = k2 · to_Pr1 DS -> k1 · to_Pr2 DS = k2 · to_Pr2 DS -> k1 = k2. Proof. intros H1 H2. rewrite (ToBinDirectSumUnique DS (k1 · to_Pr1 DS) (k1 · to_Pr2 DS) k1). apply pathsinv0. apply ToBinDirectSumUnique. - apply pathsinv0. apply H1. - apply pathsinv0. apply H2. - apply idpath. - apply idpath. 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.