Lemma InvTranslationFunctorH_Mor_Comp {C1 C2 C3 : ComplexHomot_Additive A} (f : (ComplexHomot_Additive A)⟦C1, C2⟧) (g : (ComplexHomot_Additive A)⟦C2, C3⟧) : (InvTranslationFunctorHImMor (iscontrpr1 (InvTranslationFunctorH_Mor (f · g)))) = (InvTranslationFunctorHImMor (iscontrpr1 (InvTranslationFunctorH_Mor f))) · (InvTranslationFunctorHImMor (iscontrpr1 (InvTranslationFunctorH_Mor g))) . Proof. use (squash_to_prop (ComplexHomotFunctor_issurj A f)). { use to_has_homsets. } intros f'. use (squash_to_prop (ComplexHomotFunctor_issurj A g)). { use to_has_homsets. } intros g'. rewrite (InvTranslationFunctorHImEq (iscontrpr1 (InvTranslationFunctorH_Mor f)) _ (hfiberpr2 _ _ f')). rewrite (InvTranslationFunctorHImEq (iscontrpr1 (InvTranslationFunctorH_Mor g)) _ (hfiberpr2 _ _ g')). set (tmp := functor_comp (ComplexHomotFunctor A) (# InvTranslationFunctor (hfiberpr1 # (ComplexHomotFunctor A) f f')) (# InvTranslationFunctor (hfiberpr1 # (ComplexHomotFunctor A) g g'))). use (pathscomp0 _ tmp). clear tmp. set (tmp := functor_comp InvTranslationFunctor (hfiberpr1 _ _ f') (hfiberpr1 _ _ g')). apply (maponpaths (# (ComplexHomotFunctor A))) in tmp. use (pathscomp0 _ tmp). clear tmp. use (InvTranslationFunctorHImEq (iscontrpr1 (InvTranslationFunctorH_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.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.