Lemma KAInvRotDTris_Comm1 (D : @DTri KAPreTriangData) (I : KADTriData D) (I' := hfiberpr1 # (ComplexHomotFunctor A) (KADTriDataMor I) (KADTriDataFiber I)) : (identity _) · (# (ComplexHomotFunctor A) ((to_inv (# (InvTranslationFunctor A) (MappingConePr1 A I'))) · TranslationEquivUnitInv A (Source (KADTriDataMor I)))) = (to_inv (# (AddEquiv2 (TranslationHEquiv A)) (# (ComplexHomotFunctor A) (MappingConePr1 A I')))) · # (ComplexHomotFunctor A) (TranslationEquivUnitInv A (Source (KADTriDataMor I))) · identity (Source (KADTriDataMor I)). Proof. use (! (KAIdComm _ _ _)). use (pathscomp0 _ (! (functor_comp (ComplexHomotFunctor A) (to_inv (# (InvTranslationFunctor A) (MappingConePr1 A I'))) (inv_from_z_iso (AddEquivUnitIso (TranslationEquiv A) (Source (KADTriDataMor I))))))). set (tmp''' := @AdditiveFunctorInv _ _ (ComplexHomotFunctor A) _ _ (# (InvTranslationFunctor A) (MappingConePr1 A I'))). apply (maponpaths (postcompose (# (ComplexHomotFunctor A) (inv_from_z_iso (AddEquivUnitIso (TranslationEquiv A) (Source (KADTriDataMor I))))))) in tmp'''. use (pathscomp0 _ (! tmp''')). clear tmp'''. unfold postcompose. apply cancel_postcomposition. apply maponpaths. use InvTranslationFunctorHImEq. 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.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.