Lemma KAOctaComm4' {x y z : Complex A} (f1 : Morphism x y) (f2 : Morphism y z) : # (ComplexHomotFunctor A) (KAOctaMor2 f1 f2) · # (ComplexHomotFunctor A) (MappingConePr1 A f2) = # (ComplexHomotFunctor A) (MappingConePr1 A (MorphismComp f1 f2)) · # (AddEquiv1 (TranslationHEquiv A)) (# (ComplexHomotFunctor A) f1). Proof. use (pathscomp0 (! (functor_comp (ComplexHomotFunctor A) _ _))). set (tmp := (KAOctaComm4 f1 f2)). apply (maponpaths (# (ComplexHomotFunctor A))) in tmp. use (pathscomp0 tmp). clear tmp. use (pathscomp0 ((functor_comp (ComplexHomotFunctor A) _ _))). apply cancel_precomposition. unfold AddEquiv1, TranslationHEquiv. cbn. apply pathsinv0. use TranslationFunctorHImEq. 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.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. Require Import UniMath.HomologicalAlgebra.TranslationFunctors.