Lemma RotMorphismIsoEq2'' {C1 C2 : Complex A} (f : Morphism C1 C2) : to_binop ((MappingCone A (MappingConeIn2 A f)) : (ComplexPreCat_Additive A)) ((MappingCone A (MappingConeIn2 A f)) : (ComplexPreCat_Additive A)) (@identity (ComplexPreCat_Additive A) (MappingCone A (MappingConeIn2 A f))) (to_inv ((RotMorphismInv f : (ComplexPreCat_Additive A)⟦_, _⟧) · RotMorphism f)) = ComplexHomotMorphism A (RotMorphismIsoHomot f). Proof. use MorphismEq. intros i. cbn. apply pathsinv0. use (pathscomp0 _ (RotMorphismIsoEq2'_eq f i)). use maponpaths_12. - exact (RotMorphismIsoEq2''_1 f i). - unfold RotMorphismIsoHomot. unfold MappingConeDiff. unfold MappingConeDiff1, MappingConeDiff2, MappingConeDiff3. cbn. unfold DiffTranslationComplex. set (DS1 := to_BinDirectSums A (C1 (i + 1)) (C2 i)). set (DS2 := to_BinDirectSums A (C2 (i + 1)) DS1). set (DS3 := to_BinDirectSums A (C1 (i + 1 + 1)) (C2 (i + 1))). set (DS4 := to_BinDirectSums A (C2 (i + 1 + 1)) DS3). set (DS5 := to_BinDirectSums A (C1 (i - 1 + 1 + 1)) (C2 (i - 1 + 1))). set (DS6 := to_BinDirectSums A (C2 (i - 1 + 1 + 1)) DS5). set (DS7 := to_BinDirectSums A (C1 (i - 1 + 1)) (C2 (i - 1))). set (DS8 := to_BinDirectSums A (C2 (i - 1 + 1)) DS7). set (DS9 := to_BinDirectSums A (C1 (i + 1 - 1 + 1)) (C2 (i + 1 - 1))). set (DS10 := to_BinDirectSums A (C2 (i + 1 - 1 + 1)) DS9). rewrite to_postmor_linear'. rewrite assoc. rewrite (assoc _ _ (to_In1 DS4)). rewrite <- (assoc _ (to_In1 DS4)). rewrite (to_Unel1' DS4). rewrite ZeroArrow_comp_right. rewrite ZeroArrow_comp_left. rewrite to_lunax''. rewrite assoc. rewrite (assoc _ _ (to_In2 DS4)). rewrite (assoc _ _ (to_In2 DS4)). rewrite to_postmor_linear'. rewrite <- (assoc _ (to_In2 DS4)). rewrite <- (assoc _ (to_In2 DS4)). rewrite (to_IdIn2 DS4). rewrite id_right. rewrite id_right. rewrite to_postmor_linear'. rewrite <- transport_target_to_binop. use maponpaths_12. + exact (RotMorphismIsoEq2''_2 f i). + exact (RotMorphismIsoEq2''_3 f i). 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.