Lemma AbelianPreCat_op_eq1 {X Y : A} (a b c d : X --> Y) : Abelian_minus_op (Abelian_mor_to_BinProd a b) (Abelian_mor_to_BinProd c d) = Abelian_mor_to_BinProd (Abelian_minus_op a c) (Abelian_minus_op b d). Proof. set (com1 := Abelian_op_eq (BinProductPr1 A (to_BinProducts A Y Y))). set (com2 := Abelian_op_eq (BinProductPr2 A (to_BinProducts A Y Y))). unfold Abelian_minus_op. unfold Abelian_mor_to_BinProd. use BinProductArrowsEq. - rewrite <- assoc. rewrite com1. rewrite BinProductPr1Commutes. rewrite assoc. apply cancel_postcomposition. use BinProductArrowsEq. + rewrite BinProductPr1Commutes. rewrite <- assoc. rewrite BinProductPr1Commutes. rewrite assoc. rewrite BinProductPr1Commutes. rewrite BinProductPr1Commutes. apply idpath. + rewrite BinProductPr2Commutes. rewrite <- assoc. rewrite BinProductPr2Commutes. rewrite assoc. rewrite BinProductPr2Commutes. rewrite BinProductPr1Commutes. apply idpath. - rewrite <- assoc. rewrite com2. rewrite BinProductPr2Commutes. rewrite assoc. apply cancel_postcomposition. use BinProductArrowsEq. + rewrite BinProductPr1Commutes. rewrite <- assoc. rewrite BinProductPr1Commutes. rewrite assoc. rewrite BinProductPr1Commutes. rewrite BinProductPr2Commutes. apply idpath. + rewrite BinProductPr2Commutes. rewrite <- assoc. rewrite BinProductPr2Commutes. rewrite assoc. rewrite BinProductPr2Commutes. 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.