Definition make_abgr_isKernel_Criteria {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) : ∑ ψ : abgr_Abelian ⟦W, X⟧, ψ · f = h. Proof. use tpair. - use monoidfunconstr. + intros w'. exact (pr1 (iscontrpr1 (abgr_isKernel_iscontr f g ZA H isM h H' w'))). + exact (abgr_isKernel_Criteria_ismonoidfun f g ZA H isM h H'). - exact (abgr_isKernel_Criteria_comm f g ZA H isM h H'). Defined.
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.