proposition: Lemma isAdditiveCriteria_isZero {A B : CategoryWithAdditiveStructure} (F : functor A B) (H : PreservesBinDirectSums F) : isZero (F (to_Zero A)).
proof: 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.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.Algebra.BinaryOperations UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.CategoriesWithBinOps UniMath.CategoryTheory.PrecategoriesWithAbgrops UniMath.CategoryTheory.PreAdditive UniMath.CategoryTheory.Additive UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Equivalences.Core UniMath.CategoryTheory.Limits.Zero UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.BinDirectSums