proposition: 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: 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.
imports: UniMath.Foundations.UnivalenceAxiom UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.PartA UniMath.Algebra.BinaryOperations UniMath.Algebra.Monoids UniMath.NumberSystems.Integers UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.TransportMorphisms UniMath.CategoryTheory.Limits.Zero UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Equalizers UniMath.CategoryTheory.Limits.Coequalizers UniMath.CategoryTheory.Limits.Kernels UniMath.CategoryTheory.Limits.Cokernels UniMath.CategoryTheory.Limits.Pushouts UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.Limits.BinDirectSums UniMath.CategoryTheory.Monics UniMath.CategoryTheory.Epis UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Equivalences.Core UniMath.CategoryTheory.CategoriesWithBinOps UniMath.CategoryTheory.PrecategoriesWithAbgrops UniMath.CategoryTheory.PreAdditive UniMath.CategoryTheory.Additive UniMath.CategoryTheory.Abelian UniMath.CategoryTheory.AbelianToAdditive UniMath.CategoryTheory.AdditiveFunctors UniMath.HomologicalAlgebra.Complexes UniMath.HomologicalAlgebra.KA UniMath.HomologicalAlgebra.TranslationFunctors