Lemma AbelianPreCat_homset_assoc_eq2 {X Y : A} (f g : X --> Y) : Abelian_minus_op (AbelianPreCat_homset_zero X Y) (Abelian_op _ _ f g) = Abelian_minus_op (Abelian_minus_op (AbelianPreCat_homset_zero X Y) f) g. Proof. set (tmp := AbelianPreCat_homset_inv_left' (AbelianPreCat_homset_zero X Y)). apply (maponpaths (λ h : _, Abelian_minus_op h (Abelian_op X Y f g))) in tmp. apply pathsinv0 in tmp. use (pathscomp0 tmp). unfold Abelian_op. rewrite AbelianPreCat_op_eq3. set (tmp2 := AbelianPreCat_homset_zero_left g). unfold Abelian_op in tmp2. rewrite tmp2. 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.