Lemma Abelian_DiagonalMap_eq {X Y : A} (f : X --> Y) : f · (DiagonalMap (to_BinProducts A Y Y)) = (DiagonalMap (to_BinProducts A X X)) · (BinProductArrow A (to_BinProducts A Y Y) (BinProductPr1 _ (to_BinProducts A X X) · f) (BinProductPr2 _ (to_BinProducts A X X) · f)). Proof. unfold DiagonalMap. use BinProductArrowsEq. - repeat rewrite <- assoc. rewrite BinProductPr1Commutes. rewrite BinProductPr1Commutes. rewrite assoc. rewrite BinProductPr1Commutes. rewrite id_left. apply id_right. - repeat rewrite <- assoc. rewrite BinProductPr2Commutes. rewrite BinProductPr2Commutes. rewrite assoc. rewrite BinProductPr2Commutes. rewrite id_left. 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.