Lemma AbelianPreCat_homset_zero_right {X Y : A} (f : X --> Y) : Abelian_op _ _ f (AbelianPreCat_homset_zero X Y) = f. Proof. unfold AbelianPreCat_homset_zero. unfold Abelian_op. unfold Abelian_minus_op at 2. use (pathscomp0 _ (AbelianPreCat_homset_zero_right' f)). set (bpY := to_BinProducts A Y Y). assert (e : (BinProductArrow A bpY (ZeroArrow (to_Zero A) X Y) (ZeroArrow (to_Zero A) X Y)) · CokernelArrow (CokernelOfDiagonal bpY) = ZeroArrow (to_Zero A) _ _ ). { use (pathscomp0 _ (ZeroArrow_comp_left A (to_Zero A) _ _ _ (CokernelArrow (CokernelOfDiagonal bpY)))). apply cancel_postcomposition. use BinProductArrowsEq. - rewrite BinProductPr1Commutes. rewrite ZeroArrow_comp_left. apply idpath. - rewrite BinProductPr2Commutes. rewrite ZeroArrow_comp_left. apply idpath. } rewrite e. 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.