Lemma AdditiveFunctorPreservesBinDirectSums {A B : CategoryWithAdditiveStructure} (F : AdditiveFunctor A B) : PreservesBinDirectSums F. Proof. intros a1 a2 DS. use make_isBinDirectSum. - use (AdditiveFunctorPreservesBinDirectSums_idin1 F DS). - use (AdditiveFunctorPreservesBinDirectSums_idin2 F DS). - use (AdditiveFunctorPreservesBinDirectSums_unit1 F DS). - use (AdditiveFunctorPreservesBinDirectSums_unit2 F DS). - use (AdditiveFunctorPreservesBinDirectSums_id F DS). 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.