proposition: Lemma SwitchMapMapEqn {M:PreAdditive} {a b c d:M} (ac : BinDirectSum a c) (ca : BinDirectSum c a) (bd : BinDirectSum b d) (db : BinDirectSum d b) (f : a --> b) (g : c --> d) : SwitchMap c a ca ac · directSumMap ac bd f g = directSumMap ca db g f · SwitchMap d b db bd.
proof: Proof. unfold SwitchMap. rewrite leftDistribute. rewrite assoc'. rewrite directSumMapEqIn2. rewrite assoc. rewrite rightDistribute. rewrite assoc. rewrite directSumMapEqPr1. apply maponpaths. rewrite assoc'. rewrite directSumMapEqIn1. rewrite assoc. rewrite assoc. rewrite directSumMapEqPr2. reflexivity. 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