Lemma MappingConeMorExtComm {C1 C1' C2 C2' : Complex A} (f : Morphism C1 C2) (f' : Morphism C1' C2') (g1 : Morphism C1 C1') (g2 : Morphism C2 C2') (H : ComplexHomot A C1 C2') (Comm : to_binop _ _ ((f : (ComplexPreCat_Additive A)⟦_, _⟧) · g2) (to_inv ((g1 : (ComplexPreCat_Additive A)⟦_, _⟧) · f')) = ComplexHomotMorphism A H) (i : hz) : MappingConeMorExtMor f f' g1 g2 H i · MappingConeDiff A f' i = MappingConeDiff A f i · MappingConeMorExtMor f f' g1 g2 H (i + 1). Proof. set (Comm' := MorphismEq' A _ _ Comm). cbn in Comm'. unfold MappingConeMorExtMor. unfold MappingConeDiff. cbn. unfold MappingConeDiff1, MappingConeDiff2, MappingConeDiff3. cbn. unfold MappingConeMorExtMor. cbn. set (DS1 := to_BinDirectSums A (C1' (i + 1)) (C2' i)). set (DS2 := to_BinDirectSums A (C1 (i + 1)) (C2 i)). set (DS3 := to_BinDirectSums A (C1' (i + 1 + 1)) (C2' (i + 1))). set (DS4 := to_BinDirectSums A (C1 (i + 1 + 1)) (C2 (i + 1))). 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 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 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_Pr2 DS4)). rewrite <- (assoc _ _ (to_Pr2 DS4)). rewrite <- (assoc _ _ (to_Pr2 DS4)). rewrite <- (assoc _ _ (to_Pr1 DS4)). rewrite <- (assoc _ _ (to_Pr1 DS4)). rewrite <- (assoc _ _ (to_Pr1 DS4)). rewrite (to_IdIn1 DS4). rewrite (to_IdIn2 DS4). rewrite (to_Unel1' DS4). rewrite (to_Unel2' DS4). unfold DiffTranslationComplex. rewrite ZeroArrow_comp_right. rewrite ZeroArrow_comp_right. rewrite ZeroArrow_comp_right. rewrite ZeroArrow_comp_left. rewrite ZeroArrow_comp_left. rewrite ZeroArrow_comp_left. rewrite ZeroArrow_comp_left. rewrite id_right. rewrite id_right. rewrite id_right. rewrite to_lunax''. rewrite to_runax''. rewrite to_runax''. rewrite ZeroArrow_comp_left. rewrite ZeroArrow_comp_left. rewrite to_lunax''. rewrite <- (assoc _ _ (to_Pr2 DS1)). rewrite <- (assoc _ _ (to_Pr2 DS1)). rewrite <- (assoc _ _ (to_Pr2 DS1)). rewrite <- (assoc _ _ (to_Pr1 DS1)). rewrite <- (assoc _ _ (to_Pr1 DS1)). rewrite <- (assoc _ _ (to_Pr1 DS1)). rewrite (to_IdIn1 DS1). rewrite (to_IdIn2 DS1). rewrite (to_Unel1' DS1). rewrite (to_Unel2' DS1). rewrite ZeroArrow_comp_right. rewrite ZeroArrow_comp_right. rewrite ZeroArrow_comp_right. rewrite ZeroArrow_comp_left. rewrite ZeroArrow_comp_left. rewrite ZeroArrow_comp_left. rewrite ZeroArrow_comp_left. rewrite ZeroArrow_comp_left. rewrite ZeroArrow_comp_left. rewrite id_right. rewrite id_right. rewrite id_right. rewrite to_runax''. rewrite to_runax''. rewrite to_runax''. rewrite to_lunax''. use maponpaths_12. - apply cancel_postcomposition. rewrite <- assoc. rewrite <- assoc. apply cancel_precomposition. rewrite <- PreAdditive_invlcomp. rewrite <- PreAdditive_invrcomp. apply maponpaths. exact (MComm g1 (i + 1)). - rewrite <- to_assoc. rewrite <- to_assoc. use maponpaths_12. + rewrite <- to_postmor_linear'. rewrite <- to_postmor_linear'. apply cancel_postcomposition. rewrite <- assoc. rewrite <- assoc. rewrite <- assoc. rewrite <- assoc. rewrite <- to_premor_linear'. rewrite <- to_premor_linear'. apply cancel_precomposition. rewrite <- PreAdditive_invlcomp. rewrite <- transport_target_postcompose. assert (e : (transportf (precategory_morphisms (C1 (i + 1))) (maponpaths C2' (hzrplusminus i 1)) (H (i + 1)) · Diff C2' i) = (transportf (precategory_morphisms (C1 (i + 1))) (maponpaths C2' (hzrminusplus (i + 1) 1)) (H (i + 1) · Diff C2' (i + 1 - 1)))). { rewrite transport_target_postcompose. rewrite transport_compose. apply cancel_precomposition. apply pathsinv0. rewrite <- maponpathsinv0. use (pathscomp0 _ (transport_hz_section A C2' 1 (Diff C2') _ _ (hzrplusminus i 1))). use transportf_paths. apply maponpaths. apply isasethz. } cbn in e. rewrite e. clear e. use (to_lcan A (transportf (precategory_morphisms (C1 (i + 1))) (maponpaths C2' (hzrplusminus (i + 1) 1)) (Diff C1 (i + 1) · H (i + 1 + 1)))). rewrite <- to_assoc. rewrite <- to_assoc. rewrite (@to_rinvax' A (Additive.to_Zero A)). rewrite to_lunax''. rewrite to_commax'. rewrite <- to_assoc. use (to_rcan A (to_inv (g1 (i + 1) · f' (i + 1)))). rewrite to_assoc. rewrite (@to_rinvax' A (Additive.to_Zero A)). rewrite to_runax''. apply pathsinv0. exact (Comm' (i + 1)). + apply cancel_postcomposition. rewrite <- assoc. rewrite <- assoc. apply cancel_precomposition. exact (MComm g2 i). 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.