Definition InvRotMorphismIsoHomot {C1 C2 : Complex A} (f : Morphism C1 C2) : ComplexHomot A (MappingCone A (to_inv (# (InvTranslationFunctor A) (MappingConePr1 A f)) · inv_from_z_iso (AddEquivUnitIso (TranslationEquiv A) C1))) (MappingCone A (to_inv (# (InvTranslationFunctor A) (MappingConePr1 A f)) · inv_from_z_iso (AddEquivUnitIso (TranslationEquiv A) C1))). Proof. intros i. cbn. use compose. - exact (C1 i). - exact (to_Pr2 (to_BinDirectSums A (to_BinDirectSums A (C1 (i + 1 - 1 + 1)) (C2 (i + 1 - 1))) (C1 i))). - use compose. + exact (to_BinDirectSums A (C1 (i - 1 + 1 - 1 + 1)) (C2 (i - 1 + 1 - 1))). + exact (transportf (λ x' : ob A, precategory_morphisms x' (to_BinDirectSums A (C1 (i - 1 + 1 - 1 + 1)) (C2 (i - 1 + 1 - 1)))) (maponpaths C1 (hzrminusplus (i - 1 + 1) 1 @ hzrminusplus i 1)) (to_In1 (to_BinDirectSums A (C1 (i - 1 + 1 - 1 + 1)) (C2 (i - 1 + 1 - 1))))). + exact (to_In1 (to_BinDirectSums A (to_BinDirectSums A (C1 (i - 1 + 1 - 1 + 1)) (C2 (i - 1 + 1 - 1))) (C1 (i - 1)))). Defined.
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.