Lemma abgr_isKernel_Criteria_uniqueness {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) (t : ∑ ψ : abgr_Abelian ⟦W, X⟧, ψ · f = h) : t = make_abgr_isKernel_Criteria f g ZA H isM h H'. Proof. use total2_paths_f. - use monoidfun_paths. use funextfun. intros x. use (abgr_monic_paths f isM). use (pathscomp0 (toforallpaths _ _ _ (base_paths _ _ (pr2 t)) x)). use pathsinv0. exact (pr2 (iscontrpr1 (abgr_isKernel_iscontr f g ZA H isM h H' (x%multmonoid)))). - use proofirrelevance. use setproperty. 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.