Lemma abgr_isKernel_Criteria_ismonoidfun {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) : ismonoidfun (λ w' : (W : abgr), pr1 (iscontrpr1 (abgr_isKernel_iscontr f g ZA H isM h H' w'))). Proof. use make_ismonoidfun. - use make_isbinopfun. intros x y. use (abgr_monic_paths f isM). use (pathscomp0 _ (! binopfunisbinopfun (f : monoidfun _ _) _ _)). use (pathscomp0 (pr2 (iscontrpr1 (abgr_isKernel_iscontr f g ZA H isM h H' ((x * y)%multmonoid))))). use (pathscomp0 (binopfunisbinopfun (h : monoidfun _ _) _ _)). use pathsinv0. use two_arg_paths. + exact (pr2 (iscontrpr1 (abgr_isKernel_iscontr f g ZA H isM h H' (x%multmonoid)))). + exact (pr2 (iscontrpr1 (abgr_isKernel_iscontr f g ZA H isM h H' (y%multmonoid)))). - use (abgr_monic_paths f isM). use (pathscomp0 (pr2 (iscontrpr1 (abgr_isKernel_iscontr f g ZA H isM h H' (unel (W : abgr)))))). use (pathscomp0 (monoidfununel h)). exact (! monoidfununel f). 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.