Lemma AbelianToisPreAdditive : isPreAdditive AbelianTocategoryWithAbgrops. Proof. use make_isPreAdditive. - intros x y z f. split. + intros x' x'0. unfold to_premor. cbn. unfold Abelian_op. unfold Abelian_minus_op. cbn in x', x'0. rewrite assoc. apply cancel_postcomposition. set (bpz := to_BinProducts A z z). assert (e : BinProductArrow A bpz (f · x') ((BinProductArrow A bpz (ZeroArrow (to_Zero A) x z) (f · x'0)) · CokernelArrow (CokernelOfDiagonal bpz)) = BinProductArrow A bpz (f · x') ((BinProductArrow A bpz (f · ZeroArrow (to_Zero A) y z) (f · x'0)) · CokernelArrow (CokernelOfDiagonal bpz))). { set (tmp := ZeroArrow_comp_right A (to_Zero A) x y z f). apply (maponpaths (λ h : _, BinProductArrow A bpz (f · x') ((BinProductArrow A bpz h (f · x'0)) · CokernelArrow (CokernelOfDiagonal bpz)))) in tmp. apply pathsinv0 in tmp. apply tmp. } use (pathscomp0 _ (!e)). clear e. rewrite <- precompWithBinProductArrow. rewrite <- assoc. rewrite <- precompWithBinProductArrow. apply idpath. + unfold to_premor. cbn. unfold AbelianPreCat_homset_zero. apply ZeroArrow_comp_right. - intros x y z f. split. + intros x' x'0. unfold to_postmor. cbn. unfold Abelian_op. unfold Abelian_minus_op. cbn in x', x'0. set (bpz := to_BinProducts A z z). assert (e : BinProductArrow A bpz (ZeroArrow (to_Zero A) x z) (x'0 · f) = (BinProductArrow A (to_BinProducts A y y) (ZeroArrow (to_Zero A) x y) x'0) · Abelian_mor_from_to_BinProd f f). { use BinProductArrowsEq. - unfold Abelian_mor_from_to_BinProd. rewrite <- assoc. rewrite BinProductPr1Commutes. rewrite BinProductPr1Commutes. rewrite assoc. rewrite BinProductPr1Commutes. rewrite ZeroArrow_comp_left. apply idpath. - unfold Abelian_mor_from_to_BinProd. rewrite <- assoc. rewrite BinProductPr2Commutes. rewrite BinProductPr2Commutes. rewrite assoc. rewrite BinProductPr2Commutes. apply idpath. } rewrite e. clear e. unfold Abelian_mor_from_to_BinProd. repeat rewrite <- assoc. set (tmp := Abelian_op_eq f). cbn zeta in tmp. unfold bpz. rewrite <- tmp. repeat rewrite assoc. rewrite <- (postcompWithBinProductArrow A _ (to_BinProducts A y y)). repeat rewrite <- assoc. apply cancel_precomposition. unfold BinProductOfArrows. apply tmp. + unfold to_postmor. cbn. unfold AbelianPreCat_homset_zero. apply ZeroArrow_comp_left. 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.