proposition: Lemma AdditiveFunctorPreservesBinDirectSums_zero {A B : CategoryWithAdditiveStructure} (F : AdditiveFunctor A B) : isZero (F (to_Zero A)).
proof: 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.
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