Lemma AbelianPreCat_op_eq3 {X Y : A} (a b c d : X --> Y) : Abelian_minus_op (Abelian_minus_op a b) (Abelian_minus_op c d) = Abelian_minus_op (Abelian_minus_op a c) (Abelian_minus_op b d). Proof. unfold Abelian_minus_op at 1. set (tmp := AbelianPreCat_op_eq1 a c b d). unfold Abelian_mor_to_BinProd in tmp. rewrite <- tmp. set (com := Abelian_op_eq (CokernelArrow (CokernelOfDiagonal (to_BinProducts A Y Y)))). unfold Abelian_minus_op at 1. rewrite <- assoc. rewrite com. rewrite assoc. set (tmp1 := AbelianPreCat_op_eq2 a c b d). unfold Abelian_mor_to_BinProd, Abelian_mor_from_to_BinProd in tmp1. rewrite tmp1. apply cancel_postcomposition. unfold Abelian_minus_op. 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.