Definition CompositionIsAdditive {A1 A2 A3 : CategoryWithAdditiveStructure} (F1 : AdditiveFunctor A1 A2) (F2 : AdditiveFunctor A2 A3) : isAdditiveFunctor (functor_composite F1 F2).
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.