Lemma AdditiveFunctorPreservesBinDirectSums_zero {A B : CategoryWithAdditiveStructure} (F : AdditiveFunctor A B) : isZero (F (to_Zero A)). Proof. set (isadd0 := AdditiveFunctor_isAdditiveFunctor F (to_Zero A) (to_Zero A)). set (unel := to_unel (to_Zero A) (to_Zero A)). set (tmp := (pr2 isadd0)). cbn in tmp. set (tmp1 := PreAdditive_unel_zero A (to_Zero A) (to_Zero A) (to_Zero A)). unfold to_unel in tmp1. rewrite tmp1 in tmp. clear tmp1. assert (tmp2 : identity (to_Zero A) = ZeroArrow (to_Zero A) _ _) by apply ArrowsToZero. rewrite <- tmp2 in tmp. clear tmp2. assert (X : # F (identity (to_Zero A)) = identity (F (to_Zero A))) by apply functor_id. set (tmp2 := PreAdditive_unel_zero B (to_Zero B) (F (to_Zero A)) (F (to_Zero A))). unfold to_unel in tmp2. rewrite tmp2 in tmp. clear tmp2. assert (X0 : z_iso (F (to_Zero A)) (to_Zero B)). { exists (ZeroArrowTo (F (to_Zero A))). exists (ZeroArrowFrom (F (to_Zero A))). split. + rewrite <- X. rewrite tmp. apply ZeroArrowEq. + apply ArrowsToZero. } apply (ZIsoToisZero B (to_Zero B) X0). 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.