Lemma AdditiveEqualizerToKernel_isKernel {x y : ob A} (f g : x --> y) (E : Equalizer f g) : isKernel (to_Zero A) (EqualizerArrow E) (to_binop x y f (to_inv g)) (AdditiveEqualizerToKernel_eq1 f g E). Proof. use make_isKernel. - intros w h H'. use unique_exists. + use (EqualizerIn E). * exact h. * use (to_rcan A (h · to_inv g)). rewrite <- to_premor_linear'. rewrite <- to_premor_linear'. rewrite (@to_rinvax' A (to_Zero A)). rewrite ZeroArrow_comp_right. exact H'. + cbn. use EqualizerCommutes. + intros y0. apply to_has_homsets. + intros y0 X. cbn in X. use (EqualizerArrowisMonic E). rewrite EqualizerCommutes. 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.