Lemma abgr_isKernel_Criteria_comm {X Y Z W : abgr_category} (f : X --> Y) (g : Y --> Z) (ZA : f · g = ZeroArrow (to_Zero abgr_Abelian) _ _) (H : ∏ (D : (∑ y : pr1 Y, pr1 g y = 1%multmonoid)), ∥ ∑ (x : abgrtogr X), monoidfuntobinopfun _ _ f x = (pr1 D) ∥) (isM : @isMonic abgr_category _ _ f) (h : abgr_Abelian ⟦W, Y⟧) (H' : h · g = ZeroArrow (to_Zero abgr_Abelian) W Z) : monoidfuncomp (monoidfunconstr (abgr_isKernel_Criteria_ismonoidfun f g ZA H isM h H')) f = h. Proof. use monoidfun_paths. use funextfun. intros x. exact (pr2 (iscontrpr1 (abgr_isKernel_iscontr f g ZA H isM h H' (x%multmonoid)))). Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.Foundations.UnivalenceAxiom. Require Import UniMath.Algebra.BinaryOperations. Require Import UniMath.Algebra.Groups. Require Import UniMath.Algebra.Monoids. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.Epis. Require Import UniMath.CategoryTheory.CategoriesWithBinOps. Require Import UniMath.CategoryTheory.PrecategoriesWithAbgrops. Require Import UniMath.CategoryTheory.PreAdditive. Require Import UniMath.CategoryTheory.Additive. Require Import UniMath.CategoryTheory.Abelian. Require Import UniMath.CategoryTheory.Limits.Zero. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Require Import UniMath.CategoryTheory.Limits.Kernels. Require Import UniMath.CategoryTheory.Limits.Cokernels. Require Import UniMath.CategoryTheory.Limits.BinDirectSums. @ZeroArrowFrom abgr_category abgr_Zero A = abgrfunfromunit A.