Lemma AdditiveKernelToEqualizer_isEqualizer {x y : ob A} (f g : x --> y) (K : Kernel (to_Zero A) (to_binop _ _ f (to_inv g))) : isEqualizer f g (KernelArrow K) (AdditiveKernelToEqualizer_eq1 f g K). Proof. use make_isEqualizer. intros w h H'. use unique_exists. - use KernelIn. + exact h. + set (X := @to_premor_linear' A). rewrite X. etrans. { apply maponpaths_2. apply H'. } rewrite <- to_premor_linear'. rewrite (@to_rinvax' A (to_Zero A)). apply ZeroArrow_comp_right. - cbn. use KernelCommutes. - intros y0. apply to_has_homsets. - intros y0 X. cbn in X. use (KernelArrowisMonic _ K). etrans. 2 : { apply pathsinv0. apply KernelCommutes. } exact X. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.Algebra.Monoids. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.Epis. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.CategoriesWithBinOps. Require Import UniMath.CategoryTheory.PrecategoriesWithAbgrops. Require Import UniMath.CategoryTheory.PreAdditive. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.Limits.Zero. Require Import UniMath.CategoryTheory.Limits.Opp. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.BinProducts. 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.