Lemma AbelianPreCat_homset_inv_left' {X Y : A} (f : X --> Y) : Abelian_minus_op f f = (AbelianPreCat_homset_zero X Y). Proof. unfold AbelianPreCat_homset_zero. unfold Abelian_minus_op. set (bpY := to_BinProducts A Y Y). assert (e : BinProductArrow A bpY f f = f · BinProductArrow A bpY (identity _ ) (identity _ )). { use BinProductArrowsEq. - rewrite BinProductPr1Commutes. rewrite <- assoc. rewrite BinProductPr1Commutes. rewrite id_right. apply idpath. - rewrite BinProductPr2Commutes. rewrite <- assoc. rewrite BinProductPr2Commutes. rewrite id_right. apply idpath. } rewrite e. rewrite <- assoc. rewrite CokernelCompZero. apply ZeroArrow_comp_right. 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.