Lemma KAInvRotDTris_Comm3 (D : @DTri KAPreTriangData) (I : KADTriData D) (I' := hfiberpr1 # (ComplexHomotFunctor A) (KADTriDataMor I) (KADTriDataFiber I)) : (# (ComplexHomotFunctor A) (InvRotMorphismInv A I')) · (# (ComplexHomotFunctor A) (MappingConePr1 A ((to_inv (# (InvTranslationFunctor A) (MappingConePr1 A I'))) · TranslationEquivUnitInv A (Source (KADTriDataMor I))))) = (# (ComplexHomotFunctor A) (MappingConeIn2 A I')) · # (ComplexHomotFunctor A) (TranslationEquivCounitInv A (MappingCone A I')) · (# (AddEquiv1 (TranslationHEquiv A)) (identity ((AddEquiv2 (TranslationHEquiv A)) (MappingCone A I')))). Proof. use (pathscomp0 (! (functor_comp (ComplexHomotFunctor A) _ _))). use (pathscomp0 (maponpaths # (ComplexHomotFunctor A) (! (InvRotMorphismInvComm2 A I')))). rewrite functor_id. use (pathscomp0 _ (! (id_right _))). exact (functor_comp (ComplexHomotFunctor A) _ _). 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.NumberSystems.Integers. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. 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.Equivalences.Core. Require Import UniMath.CategoryTheory.Abelian. Require Import UniMath.CategoryTheory.ShortExactSequences. Require Import UniMath.CategoryTheory.Categories.Abgr. Require Import UniMath.CategoryTheory.CategoriesWithBinOps. Require Import UniMath.CategoryTheory.PrecategoriesWithAbgrops. Require Import UniMath.CategoryTheory.PreAdditive. Require Import UniMath.CategoryTheory.Additive. Require Import UniMath.CategoryTheory.Morphisms. Require Import UniMath.CategoryTheory.AdditiveFunctors. Require Import UniMath.HomologicalAlgebra.Complexes. Require Import UniMath.HomologicalAlgebra.Triangulated. Require Import UniMath.HomologicalAlgebra.KA. Require Import UniMath.HomologicalAlgebra.TranslationFunctors. Require Import UniMath.HomologicalAlgebra.MappingCone.