Lemma Abelian_op_eq {X Y : A} (f : X --> Y) : let bp1 := to_BinProducts A X X in let bp2 := to_BinProducts A Y Y in CokernelArrow (CokernelOfDiagonal bp1) · f = (BinProductArrow A bp2 (BinProductPr1 _ bp1 · f) (BinProductPr2 _ bp1 · f)) · (CokernelArrow (CokernelOfDiagonal bp2)). Proof. set (bpX := to_BinProducts A X X). set (bpY := to_BinProducts A Y Y). cbn beta. cbn zeta. set (ar := (BinProductArrow A bpY (BinProductPr1 _ bpX · f) (BinProductPr2 _ bpX · f)) · (CokernelArrow (CokernelOfDiagonal bpY))). assert (H: DiagonalMap bpX · ar = ZeroArrow (to_Zero A) _ _). { unfold ar. rewrite assoc. unfold bpX, bpY. rewrite <- (Abelian_DiagonalMap_eq f). fold bpY. rewrite <- assoc. rewrite CokernelCompZero. apply ZeroArrow_comp_right. } set (g := CokernelOut (to_Zero A) (CokernelOfDiagonal bpX) (CokernelOfDiagonal bpY) ar H). set (com := CokernelCommutes (to_Zero A) (CokernelOfDiagonal bpX) (CokernelOfDiagonal bpY) ar H). rewrite <- com. apply cancel_precomposition. set (e1 := Abelian_op_eq_IdZero X). set (e2 := Abelian_op_eq_IdZero Y). set (ar' := BinProductArrow A bpY (BinProductPr1 A bpX · f) (BinProductPr2 A bpX · f)). assert (e3 : IdZeroMap (to_BinProducts A X X) · ar' = f · IdZeroMap (to_BinProducts A Y Y)). { unfold ar', IdZeroMap. apply BinProductArrowsEq. - rewrite <- assoc. rewrite BinProductPr1Commutes. rewrite assoc. rewrite BinProductPr1Commutes. rewrite id_left. rewrite <- assoc. rewrite BinProductPr1Commutes. rewrite id_right. apply idpath. - rewrite <- assoc. rewrite BinProductPr2Commutes. rewrite assoc. rewrite BinProductPr2Commutes. rewrite <- assoc. rewrite BinProductPr2Commutes. rewrite ZeroArrow_comp_right. apply ZeroArrow_comp_left. } rewrite <- (id_right f). rewrite <- e2. rewrite assoc. rewrite <- e3. unfold ar'. rewrite <- assoc. fold ar. rewrite <- id_left. cbn. rewrite <- e1. rewrite <- assoc. apply cancel_precomposition. apply pathsinv0. apply com. 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.