proposition: 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: 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.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.Algebra.Monoids UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.Limits.Zero UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Equalizers UniMath.CategoryTheory.Limits.Coequalizers UniMath.CategoryTheory.Limits.Kernels UniMath.CategoryTheory.Limits.Cokernels UniMath.CategoryTheory.Limits.Pushouts UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.Limits.BinDirectSums UniMath.CategoryTheory.Monics UniMath.CategoryTheory.Epis UniMath.CategoryTheory.CategoriesWithBinOps UniMath.CategoryTheory.PrecategoriesWithAbgrops UniMath.CategoryTheory.PreAdditive UniMath.CategoryTheory.Additive UniMath.CategoryTheory.Abelian