Lemma AbelianPreCat_homset_zero_right' {X Y : A} (f : X --> Y) : Abelian_minus_op f (AbelianPreCat_homset_zero X Y) = f. Proof. unfold AbelianPreCat_homset_zero. unfold Abelian_minus_op. set (tmp := Abelian_op_eq_IdZero Y). unfold IdZeroMap in tmp. assert (e : BinProductArrow A (to_BinProducts A Y Y) f (ZeroArrow (to_Zero A) X Y) = f · BinProductArrow A (to_BinProducts A Y Y) (identity _) (ZeroArrow (to_Zero A) Y Y)). { apply BinProductArrowsEq. - rewrite BinProductPr1Commutes. rewrite <- assoc. rewrite BinProductPr1Commutes. rewrite id_right. apply idpath. - rewrite BinProductPr2Commutes. rewrite <- assoc. rewrite BinProductPr2Commutes. rewrite ZeroArrow_comp_right. apply idpath. } rewrite e. clear e. rewrite <- assoc. rewrite tmp. apply id_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.