Lemma MappingCylinder_comp {C1 C2 : Complex A} (f : Morphism C1 C2) (i : hz) : MappingCylinderDiff f i · MappingCylinderDiff f (i + 1) = ZeroArrow (Additive.to_Zero A) _ _. Proof. unfold MappingCylinderDiff. cbn. set (D11 := MappingCylinder_Diff1_Diff1 f i). set (D12 := MappingCylinder_Diff1_Diff2 f i). set (D13 := MappingCylinder_Diff1_Diff3 f i). set (D22 := MappingCylinder_Diff2_Diff2 f i). set (D23 := MappingCylinder_Diff2_Diff3 f i). set (D33 := MapingCylinder_Diff3_Diff3 f i). 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'. cbn. cbn in D11. rewrite D11. cbn in D12. rewrite D12. cbn in D13. rewrite D13. cbn in D22. rewrite D22. cbn in D23. rewrite D23. cbn in D33. rewrite D33. rewrite to_lunax''. rewrite to_lunax''. rewrite to_runax''. rewrite to_runax''. rewrite to_lunax''. rewrite to_runax''. unfold MappingCylinderDiff1. unfold MappingCylinderDiff2. unfold MappingCylinderDiff3. cbn. clear D11 D12 D13 D22 D23 D33. set (DS1 := to_BinDirectSums A (C1 (i + 1)) (C2 i)). set (DS1' := to_BinDirectSums A (C1 i) DS1). set (DS2 := to_BinDirectSums A (C1 (i + 1 + 1 + 1)) (C2 (i + 1 + 1))). set (DS2' := to_BinDirectSums A (C1 (i + 1 + 1)) DS2). set (DS3 := to_BinDirectSums A (C1 (i + 1 + 1)) (C2 (i + 1))). set (DS3' := to_BinDirectSums A (C1 (i + 1)) DS3). cbn. 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 <- PreAdditive_invlcomp. rewrite <- (assoc _ _ (to_Pr1 DS3')). rewrite (to_IdIn1 DS3'). rewrite id_right. rewrite <- (assoc _ _ (to_Pr1 DS3')). rewrite (to_Unel2' DS3'). rewrite ZeroArrow_comp_right. rewrite ZeroArrow_comp_left. rewrite ZeroArrow_comp_left. rewrite to_runax''. rewrite <- (assoc _ _ (to_Pr2 DS3')). rewrite (to_IdIn2 DS3'). rewrite id_right. rewrite to_binop_inv_inv. apply cancel_inv. rewrite inv_inv_eq. rewrite to_inv_zero. rewrite <- to_postmor_linear'. rewrite <- (ZeroArrow_comp_left _ _ _ _ _ (to_In1 DS2')). apply cancel_postcomposition. rewrite <- assoc. rewrite <- assoc. rewrite <- to_premor_linear'. rewrite <- (ZeroArrow_comp_right _ _ _ _ _ (to_Pr2 DS1')). apply cancel_precomposition. unfold MappingConeDiff. unfold MappingConeDiff1. unfold MappingConeDiff2. unfold MappingConeDiff3. cbn in *. fold DS1 DS1' DS2 DS2' DS3 DS3'. unfold DiffTranslationComplex. rewrite assoc. rewrite assoc. rewrite <- PreAdditive_invrcomp. rewrite to_postmor_linear'. rewrite <- (assoc _ _ (to_Pr1 DS3)). rewrite (to_IdIn1 DS3). rewrite id_right. cbn. rewrite to_postmor_linear'. rewrite assoc. rewrite <- (assoc _ _ (to_Pr1 DS3)). rewrite <- (assoc _ _ (to_Pr1 DS3)). rewrite (to_Unel2' DS3). rewrite ZeroArrow_comp_right. rewrite ZeroArrow_comp_right. rewrite to_runax''. rewrite to_runax''. rewrite (@to_rinvax' A (Additive.to_Zero A)). 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.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. Require Import UniMath.HomologicalAlgebra.MappingCone.