proposition: Lemma CokernelPlusIdentity {M:ExactCategory} {A B C:M} (f:A-->B) (g:B-->C) (D:M) (BD : BinDirectSum B D) (CD : BinDirectSum C D): isCokernel' f g -> isCokernel' (f · ι₁) (directSumMap BD CD g (identity D)).
proof: Proof. intros ic. split. { rewrite assoc'. rewrite directSumMapEqIn1. rewrite assoc. rewrite (pr1 ic). apply zeroLeft. } intros T h u. apply iscontraprop1. { apply invproofirrelevance. intros [r r'] [s s']. apply subtypePath_prop; cbn. assert (Q := r' @ ! s'); clear r' s' u h. apply FromBinDirectSumsEq. - assert (L := maponpaths (λ w, ι₁ · w) Q); clear Q. simpl in L. rewrite 2 assoc in L. rewrite directSumMapEqIn1 in L. rewrite 2 assoc' in L. exact (CokernelIsEpi _ g ic _ _ _ L). - assert (L := maponpaths (λ w, ι₂ · w) Q); clear Q. simpl in L. rewrite 2 assoc in L. rewrite directSumMapEqIn2 in L. rewrite 2 assoc' in L. rewrite 2 id_left in L. exact L. } assert (Q := iscontrpr1 (pr2 ic _ _ (assoc _ _ _ @ u))). induction Q as [q Q]. exists (π₁ · q + π₂ · ι₂ · h). rewrite rightDistribute. rewrite assoc. rewrite assoc. rewrite assoc. unfold directSumMap. unfold BinDirectSumIndAr. rewrite BinDirectSumPr1Commutes,BinDirectSumPr2Commutes. rewrite id_right. rewrite assoc'. rewrite Q. rewrite assoc. rewrite <- leftDistribute. refine (_ @ id_left _). apply (maponpaths (λ w, w·h)). use to_BinOpId''. 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