proposition: 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: 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.
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