Lemma CohomologyFunctorH_Mor_Comp {C1 C2 C3 : ComplexHomot_Additive (AbelianToAdditive A)} (f : ComplexHomot_Additive (AbelianToAdditive A) ⟦C1, C2⟧) (g : ComplexHomot_Additive (AbelianToAdditive A) ⟦C2, C3⟧) : (CohomologyFunctorHImMor (iscontrpr1 (CohomologyFunctorH_Mor (f · g)))) = (CohomologyFunctorHImMor (iscontrpr1 (CohomologyFunctorH_Mor f))) · (CohomologyFunctorHImMor (iscontrpr1 (CohomologyFunctorH_Mor g))) . Proof. use (squash_to_prop (ComplexHomotFunctor_issurj (AbelianToAdditive A) f)). { apply has_homsets_ComplexPreCat. } intros f'. use (squash_to_prop (ComplexHomotFunctor_issurj (AbelianToAdditive A) g)). { apply has_homsets_ComplexPreCat. } intros g'. rewrite (CohomologyFunctorHImEq (iscontrpr1 (CohomologyFunctorH_Mor f)) _ (hfiberpr2 _ _ f')). rewrite (CohomologyFunctorHImEq (iscontrpr1 (CohomologyFunctorH_Mor g)) _ (hfiberpr2 _ _ g')). set (tmp := functor_comp (CohomologyFunctor A) (hfiberpr1 _ _ f') (hfiberpr1 _ _ g')). use (pathscomp0 _ tmp). clear tmp. use (CohomologyFunctorHImEq (iscontrpr1 (CohomologyFunctorH_Mor (f · g)))). rewrite functor_comp. 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.Algebra.BinaryOperations. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups. 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.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.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.