Lemma InvRotMorphismComm3' {C1 C2 : Complex A} (f : Morphism C1 C2) : MorphismOp A (MorphismComp (InvRotMorphism f) (MappingConeIn2 A f)) (MorphismOp_inv A (MorphismComp (MappingConePr1 A (MorphismComp (MorphismOp_inv A (InvTranslationMorphism A (MappingCone A f) (TranslationComplex A C1) (MappingConePr1 A f))) (TranslationEquivUnitInv A C1))) (InvTranslationTranslationNatTrans_Mor A (MappingCone A f)))) = ComplexHomotMorphism A (InvRotMorphismComm3Homot f). Proof. use MorphismEq. intros i. cbn. unfold InvRotMorphismMor. unfold MappingConeDiff. unfold MappingConeDiff1, MappingConeDiff2, MappingConeDiff3. cbn. unfold InvRotMorphismComm3Homot. unfold DiffTranslationComplex. cbn. set (DS1 := to_BinDirectSums A (C1 (i + 1 - 1 + 1)) (C2 (i + 1 - 1))). set (DS2 := to_BinDirectSums A DS1 (C1 i)). set (DS3 := to_BinDirectSums A (C1 (i + 1)) (C2 i)). set (DS4 := to_BinDirectSums A (C1 (i - 1 + 1)) (C2 (i - 1))). set (DS5 := to_BinDirectSums A (C1 (i - 1 + 1 + 1)) (C2 (i - 1 + 1))). set (DS6 := to_BinDirectSums A (C1 (i + 1 + 1 - 1 + 1)) (C2 (i + 1 + 1 - 1))). set (DS7 := to_BinDirectSums A DS6 (C1 (i + 1))). rewrite to_premor_linear'. rewrite to_premor_linear'. rewrite to_postmor_linear'. rewrite to_postmor_linear'. rewrite to_postmor_linear'. rewrite assoc. rewrite assoc. rewrite assoc. rewrite assoc. rewrite assoc. rewrite assoc. rewrite assoc. rewrite assoc. rewrite assoc. rewrite assoc. rewrite assoc. rewrite assoc. rewrite assoc. rewrite <- transport_target_postcompose. rewrite <- transport_target_postcompose. rewrite <- transport_target_postcompose. rewrite id_right. rewrite id_right. rewrite <- (assoc _ _ (to_Pr1 DS4)). rewrite <- (assoc _ _ (to_Pr2 DS4)). rewrite <- transport_source_precompose. rewrite <- transport_source_precompose. rewrite (to_Unel1' DS4). rewrite (to_IdIn1 DS4). rewrite transport_source_ZeroArrow. rewrite ZeroArrow_comp_right. rewrite ZeroArrow_comp_left. rewrite ZeroArrow_comp_left. rewrite to_runax''. rewrite <- (assoc _ _ (to_Pr2 DS7)). rewrite <- (assoc _ _ (to_Pr2 DS7)). rewrite (to_Unel1' DS7). rewrite ZeroArrow_comp_right. rewrite ZeroArrow_comp_left. rewrite to_lunax''. rewrite (to_IdIn2 DS7). rewrite id_right. rewrite <- (assoc _ _ (to_Pr2 DS7)). rewrite (to_IdIn2 DS7). rewrite id_right. rewrite <- (assoc _ _ (to_inv (Diff C1 (i - 1 + 1)))). rewrite <- transport_source_precompose. rewrite id_left. rewrite <- (assoc _ _ (f (i - 1 + 1))). rewrite <- transport_source_precompose. rewrite id_left. 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 transport_target_postcompose. rewrite transport_target_postcompose. cbn. rewrite (to_commax' A _ ((to_Pr2 DS2 · transportf (λ x' : A, A ⟦ x', C2 (i - 1 + 1) ⟧) (maponpaths C1 (hzrminusplus i 1)) (f (i - 1 + 1)) · transportf (precategory_morphisms (C2 (i - 1 + 1))) (@maponpaths hz A (λ i0 : pr1 hz, to_BinDirectSums A (C1 (i0 + 1)) (C2 i0)) _ _ (hzrminusplus i 1)) (to_In2 DS5)))). rewrite to_assoc. rewrite to_assoc. use maponpaths_12. - rewrite <- assoc. rewrite <- assoc. apply cancel_precomposition. set (tmp := @transport_hz_double_section A C1 C2 f _ _ (! hzrminusplus i 1)). rewrite pathsinv0inv0 in tmp. rewrite <- tmp. clear tmp. rewrite transport_compose. apply cancel_precomposition. rewrite maponpathsinv0. rewrite pathsinv0inv0. unfold DS3, DS5. induction (hzrminusplus i 1). apply idpath. - rewrite <- transport_target_to_inv. rewrite <- transport_source_to_inv. rewrite <- PreAdditive_invrcomp. rewrite <- PreAdditive_invrcomp. rewrite <- PreAdditive_invlcomp. rewrite <- PreAdditive_invlcomp. rewrite (to_commax' A _ (to_Pr2 DS2 · Diff C1 i · transportf (precategory_morphisms (C1 (i + 1))) (@maponpaths hz A (λ i0 : pr1 hz, to_BinDirectSums A (C1 (i0 + 1)) (C2 i0)) _ _ (hzrplusminus i 1)) (transportf (λ x' : A, A ⟦ x', DS1 ⟧) (maponpaths C1 (hzrminusplus (i + 1) 1)) (to_In1 DS1)))). rewrite <- to_assoc. assert (e : (to_Pr2 DS2 · transportf (λ x' : A, A ⟦ x', C1 (i - 1 + 1 + 1) ⟧) (maponpaths C1 (hzrminusplus i 1)) (Diff C1 (i - 1 + 1)) · transportf (precategory_morphisms (C1 (i - 1 + 1 + 1))) (@maponpaths hz A (λ i0 : pr1 hz, to_BinDirectSums A (C1 (i0 + 1)) (C2 i0)) _ _ (hzrminusplus i 1)) (to_In1 DS5)) = (to_Pr2 DS2 · Diff C1 i · transportf (precategory_morphisms (C1 (i + 1))) (@maponpaths hz A (λ i0 : pr1 hz, to_BinDirectSums A (C1 (i0 + 1)) (C2 i0)) _ _ (hzrplusminus i 1)) (transportf (λ x' : A, A ⟦ x', DS1 ⟧) (maponpaths C1 (hzrminusplus (i + 1) 1)) (to_In1 DS1)))). { rewrite <- assoc. rewrite <- assoc. apply cancel_precomposition. set (tmp := @transport_hz_section A C1 1 (Diff C1) _ _ (! hzrminusplus i 1)). rewrite pathsinv0inv0 in tmp. rewrite <- tmp. clear tmp. rewrite transport_compose. apply cancel_precomposition. rewrite transport_source_target_comm. unfold DS5. unfold DS1. rewrite <- maponpathsinv0. assert (e : maponpaths C1 (! maponpaths_2 hzplus (! hzrminusplus i 1) 1) = maponpaths C1 (maponpaths_2 hzplus (hzrminusplus i 1) 1)). { apply maponpaths. apply isasethz. } rewrite e. clear e. set (tmp := @transport_hz_double_section_source_target A (λ i0 : hz, C1 (i0 + 1)) (λ i0 : hz, to_BinDirectSums A (C1 (i0 + 1)) (C2 i0)) (λ i0 : hz, to_In1 (to_BinDirectSums A (C1 (i0 + 1)) (C2 i0))) _ _ (hzrminusplus i 1)). cbn in tmp. assert (e : maponpaths (λ i0 : pr1 hz, C1 (i0 + 1)) (hzrminusplus i 1) = maponpaths C1 (maponpaths_2 _ (hzrminusplus i 1) _)). { induction (hzrminusplus i 1). apply idpath. } rewrite e in tmp. clear e. use (pathscomp0 (! tmp)). clear tmp. set (tmp := @transport_hz_double_section_source_target A (λ i0 : hz, C1 (i0 + 1)) (λ i0 : hz, to_BinDirectSums A (C1 (i0 + 1)) (C2 i0)) (λ i0 : hz, to_In1 (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, C1 (i0 + 1)) (hzrplusminus i 1) = maponpaths C1 (hzrminusplus (i + 1) 1)). { assert (e' : maponpaths (λ i0 : pr1 hz, C1 (i0 + 1)) (hzrplusminus i 1) = maponpaths C1 (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. } apply (maponpaths (λ g : _, to_binop DS2 (to_BinDirectSums A (C1 (i + 1)) (C2 i)) (to_inv (to_Pr2 DS2 · transportf (λ x' : A, A ⟦ x', C1 (i - 1 + 1 + 1) ⟧) (maponpaths C1 (hzrminusplus i 1)) (Diff C1 (i - 1 + 1)) · transportf (precategory_morphisms (C1 (i - 1 + 1 + 1))) (@maponpaths hz A (λ i0 : pr1 hz, to_BinDirectSums A (C1 (i0 + 1)) (C2 i0)) _ _ (hzrminusplus i 1)) (to_In1 DS5))) g)) in e. apply (maponpaths (λ g : _, to_binop DS2 (to_BinDirectSums A (C1 (i + 1)) (C2 i)) g ((to_inv ((to_Pr1 DS2) · (transportf (precategory_morphisms DS1) (maponpaths C1 (hzrminusplus (i + 1) 1)) (to_Pr1 DS1)) · transportf (precategory_morphisms (C1 (i + 1))) (@maponpaths hz A (λ i0 : pr1 hz, to_BinDirectSums A (C1 (i0 + 1)) (C2 i0)) _ _ (hzrplusminus i 1)) (transportf (λ x' : A, A ⟦ x', DS1 ⟧) (maponpaths C1 (hzrminusplus (i + 1) 1)) (to_In1 DS1))))))) in e. use (pathscomp0 _ e). clear e. rewrite (@to_linvax' A (Additive.to_Zero A)). rewrite to_lunax''. rewrite <- (id_right (to_Pr1 DS2)). rewrite transport_target_postcompose. rewrite PreAdditive_invrcomp. rewrite id_right. rewrite <- assoc. rewrite <- assoc. rewrite PreAdditive_invrcomp. rewrite <- to_premor_linear'. apply cancel_precomposition. rewrite to_binop_inv_comm_2. apply maponpaths. rewrite <- (to_BinOpId DS1). rewrite (to_commax' A (to_Pr1 DS1 · to_In1 DS1) _). rewrite <- transport_target_to_binop. rewrite <- to_assoc. assert (e : transportf (precategory_morphisms DS1) (maponpaths C2 (hzrplusminus i 1)) (to_Pr2 DS1) · to_In2 DS3 = (transportf (precategory_morphisms DS1) (@maponpaths hz A (λ i0 : pr1 hz, to_BinDirectSums A (C1 (i0 + 1)) (C2 i0)) _ _ (hzrplusminus i 1)) (to_Pr2 DS1 · to_In2 DS1))). { rewrite transport_compose. rewrite transport_target_postcompose. apply cancel_precomposition. unfold DS1, DS3. induction (hzrplusminus i 1). apply idpath. } cbn in e. rewrite e. clear e. rewrite (@to_linvax' A (Additive.to_Zero A)). rewrite to_lunax''. rewrite transport_compose. rewrite transport_target_postcompose. apply cancel_precomposition. rewrite transport_source_target_comm. apply maponpaths. rewrite <- maponpathsinv0. rewrite transport_f_f. rewrite <- maponpathscomp0. rewrite pathsinv0r. 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.