Lemma AbelianPreCat_homset_zero_left {X Y : A} (f : X --> Y) : Abelian_op _ _ (AbelianPreCat_homset_zero X Y) f = f. Proof. rewrite <- (AbelianPreCat_homset_inv_left' f). set (tmp := AbelianPreCat_homset_zero_right' f). apply (maponpaths (λ g : _, Abelian_op X Y (Abelian_minus_op f f) g)) in tmp. apply pathsinv0 in tmp. use (pathscomp0 tmp). unfold Abelian_op. rewrite AbelianPreCat_op_eq3. rewrite AbelianPreCat_homset_zero_right'. rewrite AbelianPreCat_homset_zero_right'. rewrite AbelianPreCat_homset_inv_left'. rewrite AbelianPreCat_homset_zero_right'. apply idpath. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.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.PrecategoryBinProduct. 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.Pushouts. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.BinDirectSums. 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. + intros y H. apply ArrowsFromZero.