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