Lemma RotMorphism_comm' {C1 C2 : Complex A} (f : Morphism C1 C2) : @to_binop (ComplexPreCat_Additive A) (MappingCone A f) (MappingCone A (MappingConeIn2 A f)) (MappingConeIn2 A (MappingConeIn2 A f)) (to_inv (((MappingConePr1 A f) : (ComplexPreCat_Additive A)⟦_, _⟧) · RotMorphism f)) = ComplexHomotMorphism A (RotMorphismCommHomot f). Proof. use MorphismEq. intros i. cbn. apply pathsinv0. use pathscomp0. - exact (to_binop (to_BinDirectSums A (C1 (i + 1)) (C2 i)) (to_BinDirectSums A (C2 (i + 1)) (to_BinDirectSums A (C1 (i + 1)) (C2 i))) (transportf (precategory_morphisms (to_BinDirectSums A (C1 (i + 1)) (C2 i))) (@maponpaths hz A (λ i0 : pr1 hz, to_BinDirectSums A (C2 (i0 + 1)) (to_BinDirectSums A (C1 (i0 + 1)) (C2 i0))) _ _ (hzrminusplus i 1)) (RotMorphismCommMor1 f i)) (transportf (precategory_morphisms (to_BinDirectSums A (C1 (i + 1)) (C2 i))) (@maponpaths hz A (λ i0 : pr1 hz, to_BinDirectSums A (C2 (i0 + 1)) (to_BinDirectSums A (C1 (i0 + 1)) (C2 i0))) _ _ (hzrplusminus i 1)) (RotMorphismCommMor2 f i))). - use maponpaths_12. + apply maponpaths. exact (RotMorphismCommHomot1 f i). + apply maponpaths. exact (RotMorphismCommHomot2 f i). - unfold RotMorphismCommMor1, RotMorphismCommMor2. cbn. 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 + 1)) (C2 (i - 1 + 1))). set (DS4 := to_BinDirectSums A (C2 (i - 1 + 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). rewrite to_premor_linear'. rewrite assoc. rewrite assoc. rewrite assoc. rewrite assoc. rewrite assoc. rewrite assoc. rewrite <- transport_target_to_binop. rewrite <- transport_target_to_binop. rewrite transport_target_postcompose. rewrite transport_target_postcompose. rewrite transport_target_postcompose. rewrite transport_target_postcompose. rewrite (to_commax' A _ (to_Pr2 DS1 · Diff C2 i · transportf (precategory_morphisms (C2 (i + 1))) (@maponpaths hz A (λ i0 : pr1 hz, to_BinDirectSums A (C2 (i0 + 1)) (to_BinDirectSums A (C1 (i0 + 1)) (C2 i0))) _ _ (hzrplusminus i 1)) (transportf (λ x' : A, A ⟦ x', DS6 ⟧) (maponpaths C2 (hzrminusplus (i + 1) 1)) (to_In1 DS6)))). rewrite to_assoc. rewrite (to_commax' A (to_Pr2 DS1 · transportf (λ x' : A, A ⟦ x', DS3 ⟧) (maponpaths C2 (hzrminusplus i 1)) (to_In2 DS3) · transportf (precategory_morphisms DS3) (@maponpaths hz A (λ i0 : pr1 hz, to_BinDirectSums A (C2 (i0 + 1)) (to_BinDirectSums A (C1 (i0 + 1)) (C2 i0))) _ _ (hzrminusplus i 1)) (to_In2 DS4))). rewrite <- to_assoc. rewrite <- to_assoc. rewrite to_assoc. rewrite <- (@to_lunax'' A (Additive.to_Zero A) _ _ (to_binop DS1 DS2 (to_In2 DS2) (to_inv (to_binop DS1 DS2 (to_Pr1 DS1 · to_inv (f (i + 1)) · to_In1 DS2) (to_Pr1 DS1 · to_In1 DS1 · to_In2 DS2))))). use maponpaths_12. + rewrite <- PreAdditive_invrcomp. rewrite <- PreAdditive_invlcomp. rewrite PreAdditive_invrcomp. rewrite <- to_premor_linear'. rewrite <- (ZeroArrow_comp_right _ _ _ _ _ (to_Pr2 DS1 · Diff C2 i)). apply cancel_precomposition. unfold DS2. unfold DS1. rewrite <- (@to_linvax' A (Additive.to_Zero A) _ _ ((transportf (precategory_morphisms (C2 (i + 1))) (@maponpaths hz A (λ i0 : pr1 hz, to_BinDirectSums A (C2 (i0 + 1)) (to_BinDirectSums A (C1 (i0 + 1)) (C2 i0))) _ _ (hzrplusminus i 1)) (transportf (λ x' : A, A ⟦ x', DS6 ⟧) (maponpaths C2 (hzrminusplus (i + 1) 1)) (to_In1 DS6))))). apply maponpaths_2, maponpaths. unfold DS4, DS3, DS6, DS5. set (tmp := @transport_hz_to_In1 A (λ i0 : hz, C2 (i0 + 1)) (λ i0 : hz, to_BinDirectSums A (C1 (i0 + 1)) (C2 i0)) _ _ (hzrminusplus i 1)). cbn in tmp. assert (e : (maponpaths C2 (maponpaths (λ i0 : pr1 hz, i0 + 1) (hzrminusplus i 1))) = (maponpaths (λ i0 : pr1 hz, C2 (i0 + 1)) (hzrminusplus i 1))). { induction (hzrminusplus i 1). apply idpath. } cbn in e. rewrite e. clear e. use (pathscomp0 (! tmp)). clear tmp. set (tmp := @transport_hz_to_In1 A (λ i0 : hz, C2 (i0 + 1)) (λ i0 : hz, to_BinDirectSums A (C1 (i0 + 1)) (C2 i0)) _ _ (hzrplusminus i 1)). cbn in tmp. use (pathscomp0 tmp). clear tmp. apply maponpaths. assert (e : (maponpaths (λ i0 : pr1 hz, C2 (i0 + 1)) (hzrplusminus i 1)) = (maponpaths C2 (hzrminusplus (i + 1) 1))). { assert (e' : maponpaths (λ i0 : pr1 hz, C2 (i0 + 1)) (hzrplusminus i 1) = maponpaths C2 (maponpaths (λ i0 : hz, i0 + 1) (hzrplusminus i 1))). { induction (hzrplusminus i 1). apply idpath. } rewrite e'. apply maponpaths. apply isasethz. } rewrite e. apply idpath. + rewrite <- to_binop_inv_inv. rewrite <- PreAdditive_invrcomp. rewrite <- PreAdditive_invlcomp. rewrite inv_inv_eq. rewrite <- to_assoc. rewrite (to_commax' A (to_In2 DS2)). rewrite to_assoc. use maponpaths_12. * apply cancel_precomposition. set (tmp := @transport_hz_to_In1 A (λ i0 : hz, C2 (i0 + 1)) (λ i0 : hz, to_BinDirectSums A (C1 (i0 + 1)) (C2 i0)) _ _ (hzrplusminus i 1)). cbn in tmp. unfold DS2, DS1. use (pathscomp0 _ (! tmp)). clear tmp. apply maponpaths. unfold DS6, DS5. assert (e : (maponpaths (λ i0 : pr1 hz, C2 (i0 + 1)) (hzrplusminus i 1)) = (maponpaths C2 (hzrminusplus (i + 1) 1))). { assert (e' : (maponpaths (λ i0 : pr1 hz, C2 (i0 + 1)) (hzrplusminus i 1)) = (maponpaths C2 (maponpaths (λ i0 : pr1 hz, i0 + 1) (hzrplusminus i 1)))). { induction (hzrplusminus i 1). apply idpath. } rewrite e'. apply maponpaths. apply isasethz. } rewrite e. apply idpath. * assert (e : to_binop DS1 DS2 (to_In2 DS2) (to_inv (to_Pr1 DS1 · to_In1 DS1 · to_In2 DS2)) = to_binop DS1 DS2 (identity _ · to_In2 DS2) (to_inv (to_Pr1 DS1 · to_In1 DS1 · to_In2 DS2))). { rewrite id_left. apply idpath. } rewrite e. clear e. rewrite <- (to_BinOpId DS1). rewrite to_postmor_linear'. rewrite to_commax'. rewrite <- to_assoc. rewrite (@to_linvax' A (Additive.to_Zero A)). rewrite to_lunax''. rewrite <- assoc. rewrite <- assoc. apply cancel_precomposition. unfold DS4, DS3, DS2, DS1. induction (hzrminusplus i 1). 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.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.