proposition: Lemma MonoPlusIdentity {M : ExactCategory} {A B:M} (f:A-->B) (C:M) (AC : BinDirectSum A C) (BC : BinDirectSum B C) : isAdmissibleMonomorphism f -> isAdmissibleMonomorphism (directSumMap AC BC f (identity C)).
proof: Proof. intro i. apply (squash_to_hProp i). intros [D [p j]]. apply hinhpr. exists D. exists (π₁ · p). apply ExactSequenceFromEpi. 2:{ apply EC_ComposeEpi. - apply Pr1IsAdmEpi. - exact (hinhpr(A,,f,,j)). } apply (squash_to_hProp (to_hasZero M)); intros Z. apply (squash_to_hProp (to_hasBinDirectSums D Z)); intros DZ. assert (m := pr1 (SumOfKernelCokernelPairs AC BC DZ (EC_ExactToKernelCokernel j : isKernelCokernelPair f p) (kerCoker10 Z C : isKernelCokernelPair (identity C) 0))). assert (R : directSumMap BC DZ p 0 · to_Pr1 DZ = to_Pr1 BC · p). { apply directSumMapEqPr1. } induction R. apply IsoWithKernel. { exact m. } exists (ι₁). split. { refine (! runax (_ --> _) _ @ ! _ @ to_BinOpId'' _). apply maponpaths. apply ThroughZeroIsZero. } { refine (to_IdIn1 DZ). } 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