Lemma AbelianPreCat_homset_assoc_eq1 {X Y : A} (f g : X --> Y) : Abelian_minus_op (AbelianPreCat_homset_zero X Y) (Abelian_minus_op f g) = Abelian_op _ _ (Abelian_minus_op (AbelianPreCat_homset_zero X Y) f) g. Proof. rewrite <- (AbelianPreCat_homset_inv_left' (AbelianPreCat_homset_zero X Y)). unfold Abelian_op. rewrite AbelianPreCat_op_eq3. rewrite (AbelianPreCat_homset_inv_left' (AbelianPreCat_homset_zero X Y)). 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.