Lemma InvRotMorphismComm {C1 C2 : Complex A} (f : Morphism C1 C2) (i : hz) : InvRotMorphismMor f i · Diff C2 i = MappingConeDiff A (MorphismComp (MorphismOp_inv A (InvTranslationMorphism A (MappingCone A f) (TranslationComplex A C1) (MappingConePr1 A f))) (TranslationEquivUnitInv A C1)) i · InvRotMorphismMor f (i + 1). Proof. unfold InvRotMorphismMor. unfold MappingConeDiff. unfold MappingConeDiff1, MappingConeDiff2, MappingConeDiff3. cbn. unfold DiffTranslationComplex. unfold InvTranslationComplex. cbn. unfold MappingConeDiff. unfold MappingConeDiff1, MappingConeDiff2, MappingConeDiff3. cbn. unfold DiffTranslationComplex. unfold InvTranslationComplex. 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 + 1 - 1 + 1)) (C2 (i + 1 + 1 - 1))). set (DS4 := to_BinDirectSums A DS3 (C1 (i + 1))). set (DS5 := to_BinDirectSums A (C1 (i + 1 - 1 + 1 + 1)) (C2 (i + 1 - 1 + 1))). rewrite to_postmor_linear'. rewrite to_postmor_linear'. rewrite to_postmor_linear'. rewrite to_premor_linear'. rewrite to_premor_linear'. rewrite to_premor_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 <- (assoc _ (to_In2 DS4)). rewrite <- (assoc _ (to_In2 DS4)). rewrite <- (assoc _ (to_In2 DS4)). rewrite <- (assoc _ (to_In2 DS4)). rewrite (to_Unel2' DS4). rewrite (to_IdIn2 DS4). rewrite id_right. rewrite id_right. rewrite ZeroArrow_comp_right. rewrite ZeroArrow_comp_right. rewrite ZeroArrow_comp_left. rewrite to_runax''. rewrite to_runax''. rewrite <- transport_target_postcompose. rewrite <- transport_target_postcompose. rewrite <- transport_target_postcompose. rewrite id_right. rewrite transport_target_to_inv. rewrite inv_inv_eq. rewrite <- transport_target_postcompose. rewrite to_premor_linear'. rewrite to_premor_linear'. rewrite assoc. rewrite assoc. rewrite assoc. rewrite assoc. rewrite assoc. rewrite assoc. rewrite <- (assoc _ (to_In1 DS4)). rewrite (to_Unel1' DS4). rewrite ZeroArrow_comp_right. rewrite ZeroArrow_comp_left. rewrite to_lunax''. rewrite <- (assoc _ (to_In1 DS4)). rewrite (to_IdIn1 DS4). rewrite id_right. rewrite <- PreAdditive_invrcomp. rewrite <- PreAdditive_invrcomp. rewrite <- PreAdditive_invlcomp. rewrite <- transport_target_to_inv. rewrite <- to_assoc. rewrite to_commax'. rewrite <- (assoc _ (Diff C1 i)). rewrite <- (MComm f i). rewrite assoc. use maponpaths_12. - rewrite transport_target_postcompose. rewrite transport_target_postcompose. rewrite transport_target_postcompose. rewrite <- transport_target_to_binop. rewrite PreAdditive_invrcomp. rewrite PreAdditive_invrcomp. rewrite transport_target_postcompose. rewrite <- transport_target_to_binop. rewrite transport_target_postcompose. rewrite transport_target_postcompose. rewrite <- (assoc (to_Pr1 DS2)). rewrite <- (assoc (to_Pr1 DS2)). rewrite <- (assoc (to_Pr1 DS2)). rewrite <- (assoc (to_Pr1 DS2)). rewrite <- (assoc (to_Pr1 DS2)). rewrite <- (assoc (to_Pr1 DS2)). rewrite <- (assoc (to_Pr1 DS2)). rewrite <- (assoc (to_Pr1 DS2)). rewrite <- to_premor_linear'. rewrite <- to_premor_linear'. rewrite <- (assoc (to_Pr1 DS2)). rewrite <- to_premor_linear'. apply cancel_precomposition. rewrite <- to_assoc. rewrite (to_commax' A _ (((to_Pr2 DS1) · (Diff C2 (i + 1 - 1)) · (transportf (precategory_morphisms (C2 (i + 1 - 1 + 1))) (@maponpaths hz A (λ i0 : pr1 hz, to_BinDirectSums A (C1 (i0 + 1)) (C2 i0)) _ _ (hzrminusplus (i + 1) 1 @ ! hzrplusminus (i + 1) 1)) (to_In2 DS5))))). rewrite to_postmor_linear'. rewrite to_assoc. set (tmp := @to_runax'' A (Additive.to_Zero A) _ _ (transportf (precategory_morphisms DS1) (maponpaths C2 (hzrplusminus i 1)) (to_Pr2 DS1) · Diff C2 i)). use (pathscomp0 (! tmp)). clear tmp. use maponpaths_12. + rewrite transport_compose. rewrite <- assoc. rewrite <- assoc. apply cancel_precomposition. rewrite <- transport_target_postcompose. rewrite <- transport_target_postcompose. rewrite assoc. rewrite <- transport_target_postcompose. rewrite <- maponpathsinv0. set (tmp := transport_hz_section A C2 1 (Diff C2) _ _ (hzrplusminus i 1)). use (pathscomp0 (! tmp)). clear tmp. apply pathsinv0. rewrite transport_target_postcompose. rewrite transport_compose. rewrite <- (id_right (Diff C2 (i + 1 - 1))). rewrite transport_target_postcompose. rewrite id_right. rewrite <- assoc. apply cancel_precomposition. rewrite <- (to_IdIn2 DS5). rewrite transport_target_postcompose. apply cancel_precomposition. assert (e : ! (@maponpaths hz A (λ i0 : pr1 hz, to_BinDirectSums A (C1 (i0 + 1)) (C2 i0)) _ _ (hzrminusplus (i + 1) 1 @ ! hzrplusminus (i + 1) 1)) = @maponpaths hz A (λ i0 : pr1 hz, to_BinDirectSums A (C1 (i0 + 1)) (C2 i0)) _ _ (! (hzrminusplus (i + 1) 1 @ ! hzrplusminus (i + 1) 1))). { rewrite maponpathsinv0. apply idpath. } rewrite e. clear e. unfold DS5. set (tmp := transport_hz_double_section A (λ (i0 : hz), to_BinDirectSums A (C1 (i0 + 1 - 1 + 1 + 1)) (C2 (i0 + 1 - 1 + 1))) (λ (i0 : hz), C2 (i0 + 1 - 1 + 1)) (λ (i0 : hz), to_Pr2 (to_BinDirectSums A (C1 (i0 + 1 - 1 + 1 + 1)) (C2 (i0 + 1 - 1 + 1)))) _ _ (! (hzrplusminus i 1))). cbn in tmp. set (e1 := maponpaths C2 (maponpaths_2 _ (hzrplusminus i 1) _)). set (e2 := maponpaths (λ i0 : pr1 hz, C2 (i0 + 1 - 1 + 1)) (! hzrplusminus i 1)). cbn in e1, e2. set (tmp' := transport_hz_double_section A (λ (i0 : hz), to_BinDirectSums A (C1 (i0 + 1)) (C2 i0)) C2 (λ (i0 : hz), to_Pr2 (to_BinDirectSums A (C1 (i0 + 1)) (C2 i0))) _ _ (maponpaths_2 hzplus (hzrplusminus i 1) 1)). cbn in tmp'. unfold e1. use (pathscomp0 _ (! tmp')). clear tmp'. unfold DS3. set (tmp' := transport_hz_double_section A (λ (i0 : hz), to_BinDirectSums A (C1 (i0 + 1)) (C2 i0)) C2 (λ (i0 : hz), to_Pr2 (to_BinDirectSums A (C1 (i0 + 1)) (C2 i0))) _ _ (hzrplusminus (i + 1) 1)). cbn in tmp'. rewrite tmp'. clear tmp'. rewrite transport_f_f. assert (e : (@maponpaths hz A (λ i0 : pr1 hz, to_BinDirectSums A (C1 (i0 + 1)) (C2 i0)) _ _ (! hzrplusminus (i + 1) 1) @ @maponpaths hz A (λ i0 : pr1 hz, to_BinDirectSums A (C1 (i0 + 1)) (C2 i0)) _ _ (! (hzrminusplus (i + 1) 1 @ ! hzrplusminus (i + 1) 1))) = @maponpaths hz A (λ i0 : pr1 hz, to_BinDirectSums A (C1 (i0 + 1)) (C2 i0)) _ _ (! maponpaths_2 _ (hzrplusminus i 1) _)). { set (tmp' := @maponpathscomp0 _ _ _ _ _ (λ i0 : pr1 hz, BinDirectSumOb (to_BinDirectSums A (C1 (i0 + 1)) (C2 i0))) (! hzrplusminus (i + 1) 1) (! (hzrminusplus (i + 1) 1 @ ! hzrplusminus (i + 1) 1))). use (pathscomp0 (! tmp')). clear tmp'. apply maponpaths. apply isasethz. } cbn in e. cbn. rewrite e. clear e. apply idpath. + rewrite to_postmor_linear'. rewrite to_assoc. rewrite to_commax'. rewrite <- (@to_runax'' A (Additive.to_Zero A) _ _ (ZeroArrow (Additive.to_Zero A) DS1 (C2 (i + 1)))). use maponpaths_12. * rewrite <- PreAdditive_invlcomp. assert (e : (to_Pr1 DS1 · f (i + 1 - 1 + 1) · transportf (precategory_morphisms (C2 (i + 1 - 1 + 1))) (@maponpaths hz A(λ i0 : pr1 hz, to_BinDirectSums A (C1 (i0 + 1)) (C2 i0)) _ _ (hzrminusplus (i + 1) 1 @ ! hzrplusminus (i + 1) 1)) (to_In2 DS5) · transportf (precategory_morphisms DS3) (maponpaths C2 (hzrplusminus (i + 1) 1)) (to_Pr2 DS3)) = (transportf (precategory_morphisms DS1) (maponpaths C1 (hzrminusplus (i + 1) 1)) (to_Pr1 DS1) · f (i + 1))). { rewrite transport_compose. rewrite <- assoc. rewrite <- assoc. apply cancel_precomposition. set (tmp := transport_hz_double_section A C1 C2 f _ _ (hzrminusplus (i + 1) 1)). rewrite <- maponpathsinv0. use (pathscomp0 _ tmp). clear tmp. rewrite <- (id_right (f (i + 1 - 1 + 1))). rewrite transport_target_postcompose. rewrite id_right. apply cancel_precomposition. rewrite <- (to_IdIn2 DS5). rewrite transport_target_postcompose. rewrite transport_compose. apply cancel_precomposition. assert (e : ! (@maponpaths hz A (λ i0 : pr1 hz, to_BinDirectSums A (C1 (i0 + 1)) (C2 i0)) _ _ (hzrminusplus (i + 1) 1 @ ! hzrplusminus (i + 1) 1)) = @maponpaths hz A (λ i0 : pr1 hz, to_BinDirectSums A (C1 (i0 + 1)) (C2 i0)) _ _ (! (hzrminusplus (i + 1) 1 @ ! hzrplusminus (i + 1) 1))). { rewrite maponpathsinv0. apply idpath. } rewrite e. clear e. unfold DS5. set (tmp' := transport_hz_double_section A (λ (i0 : hz), to_BinDirectSums A (C1 (i0 + 1)) (C2 i0)) C2 (λ (i0 : hz), to_Pr2 (to_BinDirectSums A (C1 (i0 + 1)) (C2 i0))) _ _ (hzrminusplus (i + 1) 1)). cbn in tmp'. use (pathscomp0 _ (! tmp')). clear tmp'. unfold DS3. set (tmp' := transport_hz_double_section A (λ (i0 : hz), to_BinDirectSums A (C1 (i0 + 1)) (C2 i0)) C2 (λ (i0 : hz), to_Pr2 (to_BinDirectSums A (C1 (i0 + 1)) (C2 i0))) _ _ (hzrplusminus (i + 1) 1)). cbn in tmp'. cbn. cbn in tmp'. rewrite tmp'. clear tmp'. rewrite transport_f_f. assert (e : (@maponpaths hz A (λ i0 : pr1 hz, to_BinDirectSums A (C1 (i0 + 1)) (C2 i0)) _ _ (! hzrplusminus (i + 1) 1) @ @maponpaths hz A (λ i0 : pr1 hz, to_BinDirectSums A (C1 (i0 + 1)) (C2 i0)) _ _ (! (hzrminusplus (i + 1) 1 @ ! hzrplusminus (i + 1) 1))) = @maponpaths hz A (λ i0 : pr1 hz, to_BinDirectSums A (C1 (i0 + 1)) (C2 i0)) _ _ (! hzrminusplus (i + 1) 1)). { set (tmp' := @maponpathscomp0 _ _ _ _ _ (λ i0 : pr1 hz, BinDirectSumOb (to_BinDirectSums A (C1 (i0 + 1)) (C2 i0))) (! hzrplusminus (i + 1) 1) (! (hzrminusplus (i + 1) 1 @ ! hzrplusminus (i + 1) 1))). use (pathscomp0 (! tmp')). clear tmp'. apply maponpaths. apply isasethz. } cbn in e. cbn. rewrite e. clear e. apply idpath. } apply (maponpaths (λ g : _, to_binop _ _ g (to_inv (transportf (precategory_morphisms DS1) (maponpaths C1 (hzrminusplus (i + 1) 1)) (to_Pr1 DS1) · f (i + 1))))) in e. use (pathscomp0 _ (! e)). clear e. rewrite (@to_rinvax' A (Additive.to_Zero A)). apply idpath. * rewrite <- (ZeroArrow_comp_right _ _ _ _ _ (to_Pr1 DS1 · Diff C1 (i + 1 - 1 + 1))). rewrite <- assoc. rewrite <- assoc. rewrite <- assoc. apply cancel_precomposition. apply cancel_precomposition. rewrite transport_compose. rewrite <- PreAdditive_invlcomp. rewrite <- to_inv_zero. apply maponpaths. set (DS6 := to_BinDirectSums A (C1 (i + 1 - 1 + 1 + 1)) (C2 (i + 1))). rewrite <- (to_Unel1' DS6). rewrite <- transport_compose. unfold DS3. set (tmp' := transport_hz_double_section A (λ (i0 : hz), to_BinDirectSums A (C1 (i0 + 1)) (C2 i0)) C2 (λ (i0 : hz), to_Pr2 (to_BinDirectSums A (C1 (i0 + 1)) (C2 i0))) _ _ (hzrplusminus (i + 1) 1)). cbn in tmp'. rewrite tmp'. clear tmp'. rewrite transport_compose. rewrite transport_f_f. set (e := @maponpaths hz A (λ i0 : pr1 hz, to_BinDirectSums A (C1 (i0 + 1)) (C2 i0)) _ _ (hzrplusminus (i + 1) 1)). cbn in e. unfold DS6. unfold DS5. set (e' := @maponpaths hz A (λ i0 : pr1 hz, to_BinDirectSums A (C1 (i + 1 - 1 + 1 + 1)) (C2 i0)) _ _ (hzrminusplus (i + 1) 1)). cbn in e'. set (tmp := @transport_compose' A _ _ _ _ (to_In1 (to_BinDirectSums A (C1 (i + 1 - 1 + 1 + 1)) (C2 (i + 1)))) (to_Pr2 (to_BinDirectSums A (C1 (i + 1 - 1 + 1 + 1)) (C2 (i + 1)))) (! e')). use (pathscomp0 (! tmp)). clear tmp. fold DS5 DS6. clear e. assert (e : transportf (precategory_morphisms (C1 (i + 1 - 1 + 1 + 1))) (! e') (to_In1 DS6) = to_In1 DS5). { unfold e'. unfold DS6, DS5. induction (hzrminusplus (i + 1) 1). apply idpath. } apply (maponpaths (postcompose (transportf (λ x' : A, A ⟦ x', C2 (i + 1) ⟧) (! e') (to_Pr2 DS6)))) in e. use (pathscomp0 e). clear e. unfold postcompose. apply cancel_precomposition. unfold e'. clear e'. unfold DS6. set (e1 := (! @maponpaths hz A (λ i0 : pr1 hz, to_BinDirectSums A (C1 (i + 1 - 1 + 1 + 1)) (C2 i0)) _ _ (hzrminusplus (i + 1) 1))). set (e2 := (@maponpaths hz A (λ i0 : pr1 hz, to_BinDirectSums A (C1 (i0 + 1)) (C2 i0)) _ _ (! hzrplusminus (i + 1) 1) @ ! @maponpaths hz A (λ i0 : pr1 hz, to_BinDirectSums A (C1 (i0 + 1)) (C2 i0)) _ _ (hzrminusplus (i + 1) 1 @ ! hzrplusminus (i + 1) 1))). cbn in e1, e2. induction (hzrminusplus (i + 1) 1). cbn. fold DS5. clear e1 e2. assert (e : (@maponpaths hz A (λ i0 : pr1 hz, to_BinDirectSums A (C1 (i0 + 1)) (C2 i0)) _ _ (! hzrplusminus (i + 1 - 1 + 1) 1) @ ! @maponpaths hz A (λ i0 : pr1 hz, to_BinDirectSums A (C1 (i0 + 1)) (C2 i0)) _ _ (! hzrplusminus (i + 1 - 1 + 1) 1)) = idpath _). { rewrite maponpathsinv0. rewrite <- pathscomp_inv. rewrite pathsinv0l. apply idpath. } apply (maponpaths (λ g : _, transportf (λ x : A, A ⟦ x, C2 (i + 1 - 1 + 1) ⟧) g (to_Pr2 DS5))) in e. use (pathscomp0 _ (! e)). apply idpath. - 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.