proposition: Lemma kerCokerDirectSum {M :PreAdditive} {A B:M} (S:BinDirectSum A B) : isKernelCokernelPair (to_In1 S) (to_Pr2 S).
proof: Proof. assert (E := BinDirectSum_isBinDirectSum M S). split. - exists (to_Unel1 S). intros T h H. use unique_exists; cbn beta. + exact (h · to_Pr1 S). + refine (! assoc _ _ _ @ _ @ id_right _). rewrite <- (to_BinOpId' S). rewrite rightDistribute. rewrite (assoc h (to_Pr2 S) (to_In2 S)). rewrite H; clear H. rewrite zeroLeft. apply pathsinv0. apply (runax (T-->S)). + intros k. apply to_has_homsets. + clear H. intros k e. induction e. rewrite assoc'. rewrite (to_IdIn1 S). apply pathsinv0, id_right. - exists (to_Unel1 S). intros T h H. use unique_exists; cbn beta. + exact (ι₂ · h). + refine (assoc _ _ _ @ _ @ id_left h). rewrite <- (to_BinOpId' S). rewrite leftDistribute. rewrite <- (assoc (to_Pr1 S) (to_In1 S) h). rewrite H; clear H. rewrite zeroRight. apply pathsinv0. apply (lunax (S-->T)). + intros k. apply to_has_homsets. + clear H. intros k e. induction e. rewrite assoc. rewrite (to_IdIn2 S). exact (! id_left _). 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