proposition: Lemma InvRotMorphismIso'_eq2' {C1 C2 : Complex A} (f : Morphism C1 C2) : MorphismOp A (MorphismComp (InvRotMorphism f) (InvRotMorphismInv f)) (MorphismOp_inv A (IdMor (MappingCone A (MorphismComp (MorphismOp_inv A (InvTranslationMorphism A (MappingCone A f) (TranslationComplex A C1) (MappingConePr1 A f))) (TranslationEquivUnitInv A C1))))) = ComplexHomotMorphism A (InvRotMorphismIsoHomot f).
proof: Proof. use MorphismEq. intros i. cbn. unfold MappingConeDiff. unfold MappingConeDiff1, MappingConeDiff2, MappingConeDiff3. unfold TranslationComplex, InvTranslationComplex. unfold InvRotMorphismIsoHomot. unfold DiffTranslationComplex. unfold InvRotMorphismMor, InvRotMorphismMorInv. cbn. unfold MappingConeDiff. unfold MappingConeDiff1, MappingConeDiff2, MappingConeDiff3. 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 + 1)) (C2 (i - 1 + 1 + 1 - 1))). set (DS6 := to_BinDirectSums A DS5 (C1 (i - 1 + 1))). set (DS7 := to_BinDirectSums A (C1 (i + 1 + 1 - 1 + 1)) (C2 (i + 1 + 1 - 1))). set (DS8 := to_BinDirectSums A DS7 (C1 (i + 1))). set (DS9 := to_BinDirectSums A (C1 (i + 1 - 1 + 1 - 1 + 1)) (C2 (i + 1 - 1 + 1 - 1))). set (DS10 := to_BinDirectSums A DS9 (C1 (i + 1 - 1))). set (DS11 := to_BinDirectSums A (C1 (i - 1 + 1 - 1 + 1 + 1)) (C2 (i - 1 + 1 - 1 + 1))). set (DS12 := to_BinDirectSums A (C1 (i + 1 - 1 + 1 + 1)) (C2 (i + 1 - 1 + 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 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_Pr1 DS4)). rewrite (to_IdIn1 DS4). rewrite id_right. rewrite <- (assoc _ _ (to_Pr2 DS4)). rewrite (to_Unel1' DS4). rewrite ZeroArrow_comp_right. rewrite ZeroArrow_comp_left. rewrite ZeroArrow_comp_left. rewrite to_runax''. rewrite <- (assoc _ _ (to_inv (to_Pr1 DS3))). rewrite <- transport_source_precompose. rewrite <- PreAdditive_invrcomp. rewrite <- PreAdditive_invrcomp. rewrite <- PreAdditive_invlcomp. rewrite <- transport_source_to_inv. rewrite (to_IdIn1 DS3). rewrite <- PreAdditive_invrcomp. rewrite <- PreAdditive_invlcomp. rewrite <- (assoc (to_Pr2 DS2)). rewrite <- (assoc (to_Pr2 DS2)). rewrite <- (assoc (to_Pr2 DS2)). rewrite <- (assoc (to_Pr2 DS2)). rewrite <- (assoc (to_Pr2 DS2)). rewrite <- transport_source_precompose. rewrite <- transport_source_precompose. rewrite <- transport_source_precompose. rewrite id_left. rewrite <- PreAdditive_invlcomp. rewrite <- (assoc (to_Pr2 DS2)). rewrite <- transport_source_precompose. rewrite <- (assoc _ (to_In1 DS8)). rewrite (to_Unel1' DS8). rewrite ZeroArrow_comp_right. rewrite ZeroArrow_comp_left. rewrite ZeroArrow_comp_left. rewrite to_lunax''. rewrite <- transport_target_postcompose. rewrite <- transport_target_postcompose. rewrite <- transport_target_postcompose. rewrite id_right. rewrite <- (assoc _ (to_In2 DS8)). rewrite <- (assoc _ (to_In2 DS8)). rewrite (to_IdIn2 DS8). rewrite id_right. rewrite id_right. 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_to_inv. rewrite <- transport_target_to_inv. rewrite <- transport_target_to_inv. rewrite <- transport_target_to_inv. rewrite transport_target_postcompose. rewrite transport_target_postcompose. rewrite <- PreAdditive_invrcomp. rewrite <- PreAdditive_invrcomp. rewrite <- PreAdditive_invlcomp. rewrite <- PreAdditive_invlcomp. rewrite <- PreAdditive_invlcomp. rewrite <- transport_source_to_inv. rewrite <- transport_target_to_inv. rewrite <- PreAdditive_invrcomp. rewrite inv_inv_eq. rewrite <- (transport_target_postcompose (to_In1 DS3)). rewrite to_premor_linear'. rewrite to_premor_linear'. rewrite (assoc (to_In1 DS3)). rewrite (assoc (to_In1 DS3)). rewrite (assoc (to_In1 DS3)). rewrite (assoc (to_In1 DS3)). rewrite (assoc (to_In1 DS3)). rewrite (assoc (to_In1 DS3)). rewrite (to_Unel1' DS3). rewrite ZeroArrow_comp_left. rewrite ZeroArrow_comp_left. rewrite to_runax''. rewrite (to_IdIn1 DS3). rewrite id_left. rewrite id_left. unfold DiffTranslationComplex. rewrite <- (to_BinOpId DS2). rewrite to_binop_inv_comm_2. rewrite to_binop_inv_comm_2. rewrite to_binop_inv_comm_1. rewrite to_binop_inv_comm_1. rewrite inv_inv_eq. rewrite to_binop_inv_comm_2. apply maponpaths. rewrite <- to_binop_inv_inv. rewrite to_assoc. assert (e : (to_binop DS2 DS2 (to_inv (to_Pr1 DS2 · transportf (precategory_morphisms DS1) (maponpaths C2 (hzrplusminus i 1)) (to_Pr2 DS1) · transportf (λ x' : A, A ⟦ x', DS1 ⟧) (maponpaths C2 (hzrplusminus i 1)) (to_In2 DS1) · to_In1 DS2)) (to_binop DS2 DS2 (to_Pr1 DS2 · to_In1 DS2) (to_Pr2 DS2 · to_In2 DS2))) = to_binop DS2 DS2 (to_Pr1 DS2 · to_Pr1 DS1 · to_In1 DS1 · to_In1 DS2) (to_Pr2 DS2 · to_In2 DS2)). { rewrite <- to_assoc. use maponpaths_12. - assert (e1 : to_Pr1 DS2 · to_In1 DS2 = to_binop DS2 DS2 (to_Pr1 DS2 · to_Pr1 DS1 · to_In1 DS1 · to_In1 DS2) (to_Pr1 DS2 · to_Pr2 DS1 · to_In2 DS1 · to_In1 DS2)). { rewrite <- to_postmor_linear'. rewrite <- assoc. rewrite <- assoc. rewrite <- to_premor_linear'. apply cancel_postcomposition. rewrite (to_BinOpId DS1). rewrite id_right. apply idpath. } rewrite e1. clear e1. set (tmp := @to_lunax'' A (Additive.to_Zero A) _ _ (to_Pr1 DS2 · to_Pr1 DS1 · to_In1 DS1 · to_In1 DS2)). use (pathscomp0 _ tmp). clear tmp. rewrite (to_commax' A (to_Pr1 DS2 · to_Pr1 DS1 · to_In1 DS1 · to_In1 DS2)). rewrite <- to_assoc. use maponpaths_12. + set (tmp := @to_linvax' A (Additive.to_Zero A) _ _ (to_Pr1 DS2 · to_Pr2 DS1 · to_In2 DS1 · to_In1 DS2)). use (pathscomp0 _ tmp). clear tmp. use maponpaths_12. * apply maponpaths. apply cancel_postcomposition. rewrite <- assoc. rewrite <- assoc. apply cancel_precomposition. rewrite transport_compose'. apply idpath. * apply idpath. + apply idpath. - apply idpath. } cbn in e. rewrite e. clear e. rewrite (to_commax' A _ (to_Pr2 DS2 · transportf (precategory_morphisms (C1 i)) (@maponpaths hz A (λ i0 : pr1 hz, to_BinDirectSums A (to_BinDirectSums A (C1 (i0 + 1 - 1 + 1)) (C2 (i0 + 1 - 1))) (C1 i0)) _ _ (hzrminusplus i 1)) (transportf (λ x' : A, A ⟦ x', DS6 ⟧) (maponpaths C1 (hzrminusplus (i - 1 + 1) 1 @ hzrminusplus i 1)) (transportf (precategory_morphisms (C1 (i - 1 + 1 - 1 + 1))) (maponpaths C1 (hzrminusplus (i - 1 + 1) 1)) (identity (C1 (i - 1 + 1 - 1 + 1))) · to_In2 DS6)))). rewrite (to_commax' A _ (to_Pr2 DS2 · to_In2 DS2)). rewrite <- to_assoc. rewrite (to_commax' A _ (to_Pr2 DS2 · to_In2 DS2)). rewrite to_assoc. rewrite to_assoc. use maponpaths_12. - apply cancel_precomposition. rewrite transport_source_precompose. unfold DS2, DS6. rewrite transport_source_target_comm. unfold DS1, DS5. induction (hzrminusplus i 1). cbn. rewrite pathscomp0rid. induction (hzrminusplus (i - 1 + 1) 1). cbn. rewrite id_left. apply idpath. - fold DS1 DS2. fold DS5 DS6. rewrite <- to_binop_inv_comm_2. rewrite to_commax'. rewrite <- to_assoc. rewrite (to_commax' A _ (to_Pr1 DS2 · transportf (precategory_morphisms DS1) (maponpaths C1 (hzrminusplus (i + 1) 1)) (to_Pr1 DS1) · transportf (λ x' : A, A ⟦ x', DS9 ⟧) (maponpaths C1 (hzrminusplus (i + 1 - 1 + 1) 1 @ hzrminusplus (i + 1) 1)) (to_In1 DS9) · transportf (precategory_morphisms DS9) (@maponpaths hz A (λ i0 : pr1 hz, to_BinDirectSums A (to_BinDirectSums A (C1 (i0 + 1 - 1 + 1)) (C2 (i0 + 1 - 1))) (C1 i0)) _ _ (hzrplusminus i 1)) (to_In1 DS10))). rewrite to_assoc. use maponpaths_12. + rewrite <- assoc. rewrite <- assoc. rewrite <- assoc. rewrite <- assoc. apply cancel_precomposition. rewrite transport_compose. apply cancel_precomposition. rewrite transport_source_precompose. rewrite transport_f_f. rewrite <- maponpathsinv0. rewrite <- maponpathscomp0. rewrite <- path_assoc. rewrite pathsinv0r. rewrite pathscomp0rid. rewrite <- transport_source_precompose. rewrite <- transport_target_postcompose. rewrite transport_source_target_comm. set (e := hzrplusminus (i + 1 - 1) 1). set (tmp := @transport_hz_double_section_source_target A (λ i0 : hz, C1 (i0 + 1 - 1 + 1)) (λ i0 : hz, to_BinDirectSums A (to_BinDirectSums A (C1 (i0 + 1 - 1 + 1)) (C2 (i0 + 1 - 1))) (C1 i0)) (λ i0 : hz, (to_In1 (to_BinDirectSums A (C1 (i0 + 1 - 1 + 1)) (C2 (i0 + 1 - 1)))) · (to_In1 (to_BinDirectSums A (to_BinDirectSums A (C1 (i0 + 1 - 1 + 1)) (C2 (i0 + 1 - 1))) (C1 i0)))) _ _ (hzrplusminus i 1)). cbn in tmp. unfold DS2, DS1. use (pathscomp0 tmp). clear tmp. unfold DS10, DS9. apply maponpaths. assert (e' : (maponpaths (λ i0 : pr1 hz, C1 (i0 + 1 - 1 + 1)) (hzrplusminus i 1)) = (maponpaths C1 (hzrminusplus (i + 1 - 1 + 1) 1))). { cbn. assert (e'' : maponpaths (λ i0 : pr1 hz, C1 (i0 + 1 - 1 + 1)) (hzrplusminus i 1) = maponpaths C1 (maponpaths (λ i0 : pr1 hz, i0 + 1 - 1 + 1) (hzrplusminus i 1))). { induction (hzrplusminus i 1). apply idpath. } rewrite e''. apply maponpaths. apply isasethz. } rewrite e'. apply idpath. + exact (InvRotMorphismIso'_eq2_2 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