Lemma TranslationFunctorH_isAdditiveFunctor : isAdditiveFunctor TranslationFunctorH. Proof. use make_isAdditiveFunctor'. - intros C1 C2. use (pathscomp0 _ (@AdditiveFunctorZeroArrow (ComplexPreCat_Additive A) (ComplexHomot_Additive A) (ComplexHomotFunctor A) (TranslationFunctorH C1) (TranslationFunctorH C2))). set (tmp := (@AdditiveFunctorZeroArrow (ComplexPreCat_Additive A) (ComplexPreCat_Additive A) TranslationFunctor_Additive C1 C2)). apply (maponpaths (# (ComplexHomotFunctor A))) in tmp. use (pathscomp0 _ tmp). clear tmp. use TranslationFunctorHImEq. use AdditiveFunctorZeroArrow. - intros C1 C2 f g. use (squash_to_prop (ComplexHomotFunctor_issurj A f)). { apply to_has_homsets. } intros f'. use (squash_to_prop (ComplexHomotFunctor_issurj A g)). { apply to_has_homsets. } intros g'. rewrite (TranslationFunctorH_Mor_Im f f'). rewrite (TranslationFunctorH_Mor_Im g g'). use (pathscomp0 _ (AdditiveFunctorLinear (ComplexHomotFunctor A) (# TranslationFunctor (hfiberpr1 _ _ f')) (# TranslationFunctor (hfiberpr1 _ _ g')))). set (tmp := AdditiveFunctorLinear TranslationFunctor_Additive (hfiberpr1 _ _ f') (hfiberpr1 _ _ g')). apply (maponpaths (# (ComplexHomotFunctor A))) in tmp. use (pathscomp0 _ tmp). clear tmp. use TranslationFunctorHImEq. rewrite AdditiveFunctorLinear. rewrite (hfiberpr2 _ _ f'). rewrite (hfiberpr2 _ _ g'). apply idpath. Qed.
Require Import UniMath.Foundations.UnivalenceAxiom. Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.Algebra.BinaryOperations. Require Import UniMath.Algebra.Monoids. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.TransportMorphisms. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Limits.Zero. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Require Import UniMath.CategoryTheory.Limits.Kernels. Require Import UniMath.CategoryTheory.Limits.Cokernels. Require Import UniMath.CategoryTheory.Limits.Pushouts. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.BinDirectSums. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.Epis. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.CategoriesWithBinOps. Require Import UniMath.CategoryTheory.PrecategoriesWithAbgrops. Require Import UniMath.CategoryTheory.PreAdditive. Require Import UniMath.CategoryTheory.Additive. Require Import UniMath.CategoryTheory.Abelian. Require Import UniMath.CategoryTheory.AbelianToAdditive. Require Import UniMath.CategoryTheory.AdditiveFunctors. Require Import UniMath.HomologicalAlgebra.Complexes. Require Import UniMath.HomologicalAlgebra.KA.