Lemma BinDirectSumIndArComp {a b c d e f : A} (f1 : a --> b) (f2 : b --> c) (g1 : d --> e) (g2 : e --> f) (B1 : BinDirectSum a d) (B2 : BinDirectSum b e) (B3 : BinDirectSum c f) : BinDirectSumIndAr f1 g1 B1 B2 · BinDirectSumIndAr f2 g2 B2 B3 = BinDirectSumIndAr (f1 · f2) (g1 · g2) B1 B3. Proof. rewrite BinDirectSumIndArEq1. rewrite (BinDirectSumIndArEq1 f2). rewrite (BinDirectSumIndArEq1 (f1 · f2)). unfold BinDirectSumIndArFormula. rewrite to_postmor_linear'. rewrite to_premor_linear'. rewrite assoc. rewrite assoc. rewrite assoc. rewrite assoc. rewrite assoc. rewrite assoc. rewrite <- (assoc _ (to_In1 B2)). rewrite <- (assoc _ (to_In1 B2)). rewrite (to_IdIn1 B2). rewrite id_right. rewrite (to_Unel1 B2). rewrite to_premor_unel'. rewrite to_postmor_unel'. rewrite to_postmor_unel'. rewrite to_runax'. rewrite to_premor_linear'. rewrite assoc. rewrite assoc. rewrite assoc. rewrite assoc. rewrite <- (assoc _ (to_In2 B2)). rewrite <- (assoc _ (to_In2 B2)). rewrite (to_IdIn2 B2). rewrite id_right. rewrite (to_Unel2 B2). rewrite to_premor_unel'. rewrite to_postmor_unel'. rewrite to_postmor_unel'. rewrite to_lunax'. 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.