Lemma AbelianPreCat_op_eq2 {X Y : A} (a b c d : X --> Y) : (Abelian_mor_to_BinProd (Abelian_mor_to_BinProd a b) (Abelian_mor_to_BinProd c d)) · (Abelian_mor_from_to_BinProd (CokernelArrow (CokernelOfDiagonal (to_BinProducts A Y Y))) (CokernelArrow (CokernelOfDiagonal (to_BinProducts A Y Y)))) = Abelian_mor_to_BinProd ((Abelian_mor_to_BinProd a b) · CokernelArrow (CokernelOfDiagonal (to_BinProducts A Y Y))) ((Abelian_mor_to_BinProd c d) · CokernelArrow (CokernelOfDiagonal (to_BinProducts A Y Y))). Proof. unfold Abelian_mor_to_BinProd. unfold Abelian_mor_from_to_BinProd. use BinProductArrowsEq. - rewrite BinProductPr1Commutes. rewrite <- assoc. rewrite BinProductPr1Commutes. rewrite assoc. rewrite BinProductPr1Commutes. apply idpath. - rewrite BinProductPr2Commutes. rewrite <- assoc. rewrite BinProductPr2Commutes. rewrite assoc. rewrite BinProductPr2Commutes. 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.