Lemma isAdditiveCriteria_isZero {A B : CategoryWithAdditiveStructure} (F : functor A B) (H : PreservesBinDirectSums F) : isZero (F (to_Zero A)). Proof. set (DS := to_BinDirectSums A (to_Zero A) (to_Zero A)). set (isBDS := H (to_Zero A) (to_Zero A) DS). assert (e1 : (# F (to_In1 DS)) = (# F (to_In2 DS))). { apply maponpaths. apply ArrowsFromZero. } assert (e2 : (# F (to_Pr1 DS)) = (# F (to_Pr2 DS))). { apply maponpaths. apply ArrowsToZero. } cbn in isBDS. rewrite e1 in isBDS. rewrite e2 in isBDS. clear e1 e2. set (BDS := make_BinDirectSum _ _ _ _ _ _ _ _ isBDS). use make_isZero. - intros b. use tpair. + apply (ZeroArrow (to_Zero B) _ _). + cbn. intros t. use (pathscomp0 (!(BinDirectSumIn1Commutes B BDS _ t (ZeroArrow (to_Zero B) _ _)))). use (pathscomp0 _ (BinDirectSumIn2Commutes B BDS _ t (ZeroArrow (to_Zero B) _ _))). cbn. apply cancel_precomposition. apply idpath. - intros a. use tpair. + apply (ZeroArrow (to_Zero B) _ _). + cbn. intros t. use (pathscomp0 (!(BinDirectSumPr1Commutes B BDS _ t (ZeroArrow (to_Zero B) _ _)))). use (pathscomp0 _ (BinDirectSumPr2Commutes B BDS _ t (ZeroArrow (to_Zero B) _ _))). cbn. apply cancel_postcomposition. apply idpath. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.Algebra.BinaryOperations. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.CategoriesWithBinOps. Require Import UniMath.CategoryTheory.PrecategoriesWithAbgrops. Require Import UniMath.CategoryTheory.PreAdditive. Require Import UniMath.CategoryTheory.Additive. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.Limits.Zero. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.BinDirectSums. exists (ZeroArrowFrom (F (to_Zero A))). apply ArrowsFromZero. assert (e2 : # F (ZeroArrowFrom a2) = @ZeroArrowFrom B Z (F a2)). apply (ArrowsFromZero B Z). use (FromBinDirectSumsEq B BDS); cbn.