Lemma KAOctaMor3Iso2 {x y z : Complex A} (f1 : Morphism x y) (f2 : Morphism y z) : (@to_binop (ComplexPreCat_Additive A) (MappingCone A (KAOctaMor1 f1 f2)) (MappingCone A (KAOctaMor1 f1 f2)) (MorphismComp (KAOctaMor3Inv f1 f2) (KAOctaMor3 f1 f2)) (to_inv ((IdMor (MappingCone A (KAOctaMor1 f1 f2))) : (ComplexPreCat_Additive A)⟦_, _⟧))) = (ComplexHomotMorphism A (KAOctaMor3InvHomot f1 f2)). Proof. use MorphismEq. intros i. unfold KAOctaMor3, KAOctaMor3Inv, KAOctaMor3InvMor. unfold KAOctaMor3InvHomot, MappingConeDiff. unfold MappingConeDiff1, MappingConeDiff2, MappingConeDiff3. unfold TranslationComplex. unfold DiffTranslationComplex. cbn. unfold MappingConeDiff. unfold MappingConeDiff1, MappingConeDiff2, MappingConeDiff3. unfold TranslationComplex. unfold DiffTranslationComplex. cbn. set (DS1 := to_BinDirectSums A (x (i + 1 + 1)) (y (i + 1))). set (DS2 := to_BinDirectSums A (x (i + 1)) (z i)). set (DS3 := to_BinDirectSums A DS1 DS2). set (DS4 := to_BinDirectSums A (y (i + 1)) (z i)). set (DS5 := to_BinDirectSums A (x (i - 1 + 1 + 1)) (y (i - 1 + 1))). set (DS6 := to_BinDirectSums A (x (i - 1 + 1)) (z (i - 1))). set (DS7 := to_BinDirectSums A DS5 DS6). set (DS8 := to_BinDirectSums A (x (i + 1 + 1 + 1)) (y (i + 1 + 1))). set (DS9 := to_BinDirectSums A (x (i + 1 + 1)) (z (i + 1))). set (DS10 := to_BinDirectSums A DS8 DS9). set (DS11 := to_BinDirectSums A (x (i + 1 - 1 + 1 + 1)) (y (i + 1 - 1 + 1))). set (DS12 := to_BinDirectSums A (x (i + 1 - 1 + 1)) (z (i + 1 - 1))). set (DS13 := to_BinDirectSums A DS11 DS12). set (DS14 := to_BinDirectSums A (x (i - 1 + 1 + 1 + 1)) (y (i - 1 + 1 + 1))). set (DS15 := to_BinDirectSums A (x (i - 1 + 1 + 1)) (z (i - 1 + 1))). set (DS16 := to_BinDirectSums A DS14 DS15). rewrite to_postmor_linear'. rewrite to_postmor_linear'. rewrite to_postmor_linear'. 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 to_premor_linear'. rewrite to_premor_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. 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_In2 DS4)). rewrite <- (assoc _ (to_In2 DS4)). rewrite <- (assoc _ (to_In1 DS4)). rewrite <- (assoc _ (to_In1 DS4)). rewrite <- (assoc _ (to_In1 DS4)). rewrite <- (assoc _ (to_In1 DS4)). rewrite (to_Unel1' DS4). rewrite (to_Unel2' DS4). rewrite (to_IdIn1 DS4). rewrite (to_IdIn2 DS4). rewrite id_right. rewrite id_right. rewrite id_right. rewrite ZeroArrow_comp_right. rewrite ZeroArrow_comp_left. rewrite ZeroArrow_comp_left. rewrite ZeroArrow_comp_right. rewrite ZeroArrow_comp_left. rewrite ZeroArrow_comp_left. rewrite ZeroArrow_comp_right. rewrite ZeroArrow_comp_left. rewrite ZeroArrow_comp_left. rewrite to_lunax''. rewrite to_runax''. rewrite to_runax''. rewrite <- (assoc _ (to_In1 DS7)). rewrite <- (assoc _ (to_In1 DS7)). rewrite (to_IdIn1 DS7). rewrite (to_Unel1' DS7). rewrite id_right. rewrite ZeroArrow_comp_right. rewrite ZeroArrow_comp_left. rewrite ZeroArrow_comp_left. rewrite to_runax''. rewrite <- (assoc _ _ (to_Pr1 DS5)). rewrite <- (assoc _ _ (to_Pr2 DS5)). rewrite <- PreAdditive_invlcomp. rewrite <- PreAdditive_invlcomp. rewrite <- transport_source_precompose. rewrite <- transport_source_precompose. rewrite (to_IdIn1 DS5). rewrite (to_Unel1' DS5). rewrite transport_source_ZeroArrow. rewrite <- PreAdditive_invrcomp. rewrite <- PreAdditive_invrcomp. rewrite <- PreAdditive_invrcomp. rewrite <- PreAdditive_invrcomp. rewrite <- PreAdditive_invlcomp. rewrite <- PreAdditive_invlcomp. rewrite <- PreAdditive_invlcomp. rewrite <- PreAdditive_invlcomp. rewrite <- PreAdditive_invlcomp. rewrite <- PreAdditive_invlcomp. rewrite <- PreAdditive_invlcomp. rewrite <- PreAdditive_invlcomp. rewrite ZeroArrow_comp_right. rewrite ZeroArrow_comp_left. rewrite ZeroArrow_comp_left. rewrite ZeroArrow_comp_left. rewrite to_binop_inv_inv. rewrite to_runax''. rewrite to_postmor_linear'. rewrite to_postmor_linear'. rewrite to_postmor_linear'. rewrite to_postmor_linear'. rewrite <- (assoc _ (to_In1 DS10)). rewrite <- (assoc _ (to_In2 DS10)). rewrite <- (assoc _ (to_In2 DS10)). rewrite <- (assoc _ (to_In2 DS10)). rewrite (to_Unel1' DS10). rewrite (to_IdIn2 DS10). rewrite id_right. rewrite id_right. rewrite id_right. rewrite ZeroArrow_comp_right. rewrite ZeroArrow_comp_left. rewrite ZeroArrow_comp_left. rewrite ZeroArrow_comp_left. rewrite to_lunax''. rewrite <- (assoc _ (to_In1 DS9)). rewrite <- (assoc _ (to_In2 DS9)). rewrite (to_Unel2' DS9). rewrite (to_IdIn1 DS9). rewrite id_right. rewrite ZeroArrow_comp_right. rewrite ZeroArrow_comp_left. rewrite ZeroArrow_comp_left. rewrite to_runax''. unfold MappingConeDiff. unfold MappingConeDiff1, MappingConeDiff2, MappingConeDiff3. unfold TranslationComplex. unfold DiffTranslationComplex. cbn. fold DS1 DS2 DS3 DS4 DS5 DS6 DS7 DS8 DS9 DS10 DS11 DS12 DS13 DS14 DS15 DS16. rewrite inv_inv_eq. rewrite <- PreAdditive_invrcomp. rewrite <- PreAdditive_invrcomp. rewrite <- PreAdditive_invlcomp. rewrite <- PreAdditive_invlcomp. rewrite <- PreAdditive_invlcomp. rewrite <- PreAdditive_invlcomp. rewrite to_binop_inv_inv. rewrite <- PreAdditive_invrcomp. rewrite <- PreAdditive_invrcomp. rewrite to_premor_linear'. rewrite to_premor_linear'. rewrite to_premor_linear'. rewrite to_premor_linear'. rewrite to_postmor_linear'. rewrite to_postmor_linear'. rewrite to_postmor_linear'. rewrite to_postmor_linear'. rewrite to_postmor_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 <- PreAdditive_invrcomp. rewrite <- PreAdditive_invrcomp. rewrite <- PreAdditive_invlcomp. rewrite <- PreAdditive_invlcomp. rewrite <- PreAdditive_invlcomp. rewrite <- PreAdditive_invlcomp. rewrite <- (assoc _ (to_In2 DS9)). rewrite <- (assoc _ (to_In2 DS9)). rewrite (to_Unel2' DS9). rewrite ZeroArrow_comp_right. rewrite ZeroArrow_comp_left. rewrite ZeroArrow_comp_left. rewrite to_lunax''. rewrite ZeroArrow_comp_right. rewrite ZeroArrow_comp_left. rewrite ZeroArrow_comp_left. rewrite to_runax''. rewrite assoc. rewrite assoc. rewrite assoc. rewrite assoc. rewrite <- (assoc _ (to_In1 DS9)). rewrite (to_IdIn1 DS9). rewrite id_right. rewrite <- (assoc _ _ (to_Pr1 DS5)). rewrite <- (assoc _ _ (to_Pr2 DS5)). rewrite <- transport_source_precompose. rewrite <- transport_source_precompose. rewrite (to_IdIn1 DS5). rewrite (to_Unel1' DS5). rewrite transport_source_ZeroArrow. rewrite ZeroArrow_comp_right. rewrite ZeroArrow_comp_left. rewrite ZeroArrow_comp_left. rewrite ZeroArrow_comp_left. rewrite to_runax''. rewrite <- transport_target_to_binop. rewrite <- transport_target_to_binop. rewrite <- to_assoc. rewrite (to_commax' _ _ (to_Pr2 DS3 · to_Pr1 DS2 · f1 (i + 1) · to_In2 DS1 · to_In1 DS3)). rewrite to_assoc. rewrite to_assoc. rewrite <- transport_target_to_inv. rewrite <- transport_target_to_inv. rewrite <- to_binop_inv_comm_1. rewrite (to_commax' _ (to_inv (transportf (precategory_morphisms DS3) (@maponpaths hz A (λ i0 : pr1 hz, to_BinDirectSums A (to_BinDirectSums A (x (i0 + 1 + 1)) (y (i0 + 1))) (to_BinDirectSums A (x (i0 + 1)) (z i0))) _ _ (hzrminusplus i 1)) (to_Pr2 DS3 · to_Pr1 DS2 · transportf (λ x' : A, A ⟦ x', x (i - 1 + 1 + 1) ⟧) (maponpaths x (maponpaths (λ i0 : pr1 hz, i0 + 1) (hzrminusplus i 1))) (identity (x (i - 1 + 1 + 1))) · Diff x (i - 1 + 1 + 1) · to_In1 DS14 · to_In1 DS16)))). rewrite to_assoc. rewrite to_assoc. use maponpaths_12. - rewrite transport_target_postcompose. rewrite <- assoc. rewrite <- assoc. rewrite <- assoc. rewrite <- assoc. rewrite <- assoc. rewrite <- assoc. rewrite <- assoc. apply cancel_precomposition. apply cancel_precomposition. rewrite <- transport_source_precompose. rewrite id_left. unfold DS3, DS2, DS1. unfold DS16, DS15, DS14. induction (hzrminusplus i 1). apply idpath. - rewrite <- (to_BinOpId DS3). rewrite <- to_binop_inv_inv. assert (e1 : (to_Pr1 DS3 · to_In1 DS3) = (to_Pr1 DS3 · identity _ · to_In1 DS3)). { rewrite id_right. apply idpath. } rewrite e1. clear e1. assert (e2 : (to_Pr2 DS3 · to_In2 DS3) = (to_Pr2 DS3 · identity _ · to_In2 DS3)). { rewrite id_right. apply idpath. } rewrite e2. clear e2. rewrite <- (to_BinOpId DS1). rewrite <- (to_BinOpId DS2). rewrite to_premor_linear'. rewrite to_premor_linear'. rewrite to_postmor_linear'. rewrite to_postmor_linear'. rewrite assoc. rewrite assoc. rewrite assoc. rewrite assoc. rewrite <- to_binop_inv_inv. rewrite <- to_binop_inv_inv. rewrite (to_commax' _ (to_Pr2 DS3 · to_Pr2 DS2 · to_In2 DS2 · to_In2 DS3)). rewrite <- to_assoc. rewrite <- to_assoc. rewrite <- to_assoc. rewrite to_assoc. rewrite to_assoc. rewrite to_assoc. rewrite (@to_linvax' A (Additive.to_Zero A)). rewrite to_runax''. rewrite (to_commax' _ _ (to_inv (to_Pr1 DS3 · to_Pr2 DS1 · to_In2 DS1 · to_In1 DS3))). rewrite <- to_assoc. rewrite <- to_assoc. rewrite (@to_rinvax' A (Additive.to_Zero A)). rewrite to_lunax''. rewrite <- to_assoc. rewrite (to_commax' _ _ (transportf (precategory_morphisms DS3) _ _)). rewrite <- transport_target_to_binop. rewrite to_assoc. use maponpaths_12. + rewrite <- transport_target_to_inv. apply maponpaths. rewrite transport_target_postcompose. rewrite <- assoc. rewrite <- (assoc _ (transportf (λ x' : A, A ⟦ x', DS11 ⟧) (maponpaths x (maponpaths (λ i0 : pr1 hz, i0 + 1) (hzrminusplus (i + 1) 1))) (to_In1 DS11))). apply cancel_precomposition. rewrite <- transport_target_postcompose. rewrite <- transport_source_precompose. set (tmp := transport_hz_double_section_source_target A (λ i0 : hz, x (i0 + 1 + 1)) (λ i0 : hz, to_BinDirectSums A (to_BinDirectSums A (x (i0 + 1 + 1)) (y (i0 + 1))) (to_BinDirectSums A (x (i0 + 1)) (z i0))) (λ i0 : hz, ((to_In1 (to_BinDirectSums A (x (i0 + 1 + 1)) (y (i0 + 1)))) · to_In1 (to_BinDirectSums A (to_BinDirectSums A (x (i0 + 1 + 1)) (y (i0 + 1))) (to_BinDirectSums A (x (i0 + 1)) (z i0))))) _ _ (hzrplusminus i 1)). cbn in tmp. unfold DS3, DS2, DS1. use (pathscomp0 tmp). clear tmp. apply maponpaths. assert (e : (maponpaths (λ i0 : pr1 hz, x (i0 + 1 + 1)) (hzrplusminus i 1)) = (maponpaths x (maponpaths (λ i0 : pr1 hz, i0 + 1) (hzrminusplus (i + 1) 1)))). { assert (e1 : (maponpaths (λ i0 : pr1 hz, x (i0 + 1 + 1)) (hzrplusminus i 1)) = (maponpaths x (maponpaths (λ i0 : pr1 hz, i0 + 1 + 1) (hzrplusminus i 1)))). { induction (hzrplusminus i 1). apply idpath. } rewrite e1. apply maponpaths. apply isasethz. } rewrite e. apply idpath. + rewrite <- to_assoc. rewrite to_commax'. rewrite <- (@to_runax'' A (Additive.to_Zero A) _ _ (to_inv (to_Pr2 DS3 · to_Pr1 DS2 · to_In1 DS2 · to_In2 DS3))). use maponpaths_12. * apply maponpaths. rewrite transport_target_postcompose. rewrite <- assoc. rewrite <- (assoc _ (transportf (λ x' : A, A ⟦ x', x (i - 1 + 1 + 1) ⟧) (maponpaths x (maponpaths (λ i0 : pr1 hz, i0 + 1) (hzrminusplus i 1))) (identity (x (i - 1 + 1 + 1))))). rewrite <- transport_source_precompose. rewrite id_left. rewrite <- (assoc _ (transportf (λ x' : A, A ⟦ x', DS15 ⟧) (maponpaths x (maponpaths (λ i0 : pr1 hz, i0 + 1) (hzrminusplus i 1))) (to_In1 DS15))). apply cancel_precomposition. rewrite <- transport_target_postcompose. rewrite <- transport_source_precompose. unfold DS3, DS2, DS1, DS16, DS15, DS14. induction (hzrminusplus i 1). apply idpath. * rewrite <- (assoc _ _ (Diff x (i - 1 + 1 + 1))). rewrite <- transport_source_precompose. rewrite id_left. unfold DS3, DS2, DS1. rewrite <- (@to_rinvax' A (Additive.to_Zero A) _ _ ((transportf (precategory_morphisms (to_BinDirectSums A (to_BinDirectSums A (x (i + 1 + 1)) (y (i + 1))) (to_BinDirectSums A (x (i + 1)) (z i)))) (@maponpaths hz A (λ i0 : pr1 hz, to_BinDirectSums A (to_BinDirectSums A (x (i0 + 1 + 1)) (y (i0 + 1))) (to_BinDirectSums A (x (i0 + 1)) (z i0))) _ _ (hzrplusminus i 1)) (to_Pr2 (to_BinDirectSums A (to_BinDirectSums A (x (i + 1 + 1)) (y (i + 1))) (to_BinDirectSums A (x (i + 1)) (z i))) · to_Pr1 (to_BinDirectSums A (x (i + 1)) (z i)) · Diff x (i + 1) · transportf (λ x' : A, A ⟦ x', DS11 ⟧) (maponpaths x (maponpaths (λ i0 : pr1 hz, i0 + 1) (hzrminusplus (i + 1) 1))) (to_In1 DS11) · to_In1 DS13)))). apply maponpaths. apply maponpaths. fold DS1 DS2 DS3. rewrite transport_target_postcompose. rewrite transport_target_postcompose. rewrite <- assoc. rewrite <- assoc. rewrite <- assoc. rewrite <- assoc. rewrite <- assoc. rewrite <- assoc. apply cancel_precomposition. apply cancel_precomposition. set (tmp := transport_hz_section A (λ i0 : hz, x (i0 + 1)) 1 (λ i0 : hz, Diff x (i0 + 1)) _ _ (! hzrminusplus i 1)). cbn in tmp. rewrite pathsinv0inv0 in tmp. assert (e : (maponpaths (λ i0 : pr1 hz, x (i0 + 1)) (hzrminusplus i 1)) = (maponpaths x (maponpaths (λ i0 : pr1 hz, i0 + 1) (hzrminusplus i 1)))). { induction (hzrminusplus i 1). apply idpath. } rewrite e in tmp. clear e. rewrite <- tmp. clear tmp. rewrite transport_compose. apply cancel_precomposition. assert (e : (! maponpaths (λ i0 : pr1 hz, x (i0 + 1)) (maponpaths_2 hzplus (! hzrminusplus i 1) 1)) = maponpaths (λ i0 : pr1 hz, x (i0 + 1)) (maponpaths_2 _ (hzrminusplus i 1) _)). { induction (hzrminusplus i 1). apply idpath. } cbn in e. rewrite e. clear e. rewrite <- transport_target_postcompose. rewrite <- transport_target_postcompose. rewrite <- transport_source_precompose. rewrite transport_source_target_comm. set (tmp := transport_hz_double_section_source_target A (λ i0 : hz, x (i0 + 1 + 1)) (λ i0 : hz, to_BinDirectSums A (to_BinDirectSums A (x (i0 + 1 + 1)) (y (i0 + 1))) (to_BinDirectSums A (x (i0 + 1)) (z i0))) (λ i0 : hz, ((to_In1 (to_BinDirectSums A (x (i0 + 1 + 1)) (y (i0 + 1)))) · to_In1 (to_BinDirectSums A (to_BinDirectSums A (x (i0 + 1 + 1)) (y (i0 + 1))) (to_BinDirectSums A (x (i0 + 1)) (z i0))))) _ _ (hzrminusplus i 1)). cbn in tmp. unfold DS16, DS15, DS14. assert (e : maponpaths (λ i0 : pr1 hz, x (i0 + 1 + 1)) (hzrminusplus i 1) = maponpaths (λ i0 : pr1 hz, x (i0 + 1)) (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, x (i0 + 1 + 1)) (λ i0 : hz, to_BinDirectSums A (to_BinDirectSums A (x (i0 + 1 + 1)) (y (i0 + 1))) (to_BinDirectSums A (x (i0 + 1)) (z i0))) (λ i0 : hz, ((to_In1 (to_BinDirectSums A (x (i0 + 1 + 1)) (y (i0 + 1)))) · to_In1 (to_BinDirectSums A (to_BinDirectSums A (x (i0 + 1 + 1)) (y (i0 + 1))) (to_BinDirectSums A (x (i0 + 1)) (z i0))))) _ _ (hzrplusminus i 1)). use (pathscomp0 _ (! tmp)). clear tmp. apply maponpaths. assert (e : (maponpaths x (maponpaths (λ i0 : pr1 hz, i0 + 1) (hzrminusplus (i + 1) 1))) = (maponpaths (λ i0 : hz, x (i0 + 1 + 1)) (hzrplusminus i 1))). { use pathscomp0. - exact (maponpaths x (maponpaths (λ i0 : hz, i0 + 1 + 1) (hzrplusminus i 1))). - apply maponpaths. apply isasethz. - induction (hzrplusminus i 1). apply idpath. } rewrite e. clear e. 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.