proposition: Lemma SumOfExactSequences {M:ExactCategory} {A B C A' B' C':M} (AA' : BinDirectSum A A') (BB' : BinDirectSum B B') (CC' : BinDirectSum C C') {f : A --> B} {g : B --> C} {f' : A' --> B'} {g' : B' --> C'} : isExact2 f g -> isExact2 f' g' -> isExact2 (directSumMap AA' BB' f f') (directSumMap BB' CC' g g').
proof: Proof. intros i i'. apply ExactSequenceFromMono. { use SumOfCokernels. - exact (EC_ExactToCokernel i). - exact (EC_ExactToCokernel i'). } apply (squash_to_hProp (to_hasBinDirectSums A B')); intros AB'. set (j := directSumMap AB' BB' f (identity B')). set (k := directSumMap AA' AB' (identity A) f'). assert (kj : k · j = directSumMap AA' BB' f f'). { apply ToBinDirectSumUnique. - refine (! assoc _ _ _ @ _). intermediate_path (k · (π₁ · f)). + apply maponpaths. apply directSumMapEqPr1. + refine (assoc _ _ _ @ _). apply (maponpaths (postcomp_with _)). exact (directSumMapEqPr1 @ id_right _). - refine (! assoc _ _ _ @ _). intermediate_path (k · (π₂ · (identity B'))). + apply maponpaths. apply directSumMapEqPr2. + refine (assoc _ _ _ @ id_right _ @ _). apply directSumMapEqPr2. } induction kj. use (EC_ComposeMono k j). - apply IdentityPlusMono. exact (ExactToAdmMono i'). - apply MonoPlusIdentity. exact (ExactToAdmMono i). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Notations UniMath.MoreFoundations.PartA UniMath.Algebra.BinaryOperations UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Monics UniMath.CategoryTheory.Epis UniMath.CategoryTheory.Limits.Zero UniMath.CategoryTheory.Limits.Kernels UniMath.CategoryTheory.Limits.Cokernels UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.Limits.Pushouts UniMath.CategoryTheory.Limits.BinDirectSums UniMath.CategoryTheory.Limits.Opp UniMath.CategoryTheory.CategoriesWithBinOps UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.PrecategoriesWithAbgrops UniMath.CategoryTheory.PreAdditive UniMath.CategoryTheory.Morphisms UniMath.CategoryTheory.Additive UniMath.CategoryTheory.Subcategory.Full UniMath.MoreFoundations.Propositions