proposition: Lemma MappingCylinderIsoHomot_eq1 {C1 C2 : Complex A} (f : (ComplexPreCat_Additive A)⟦C1, C2⟧) (i : hz) : (transportf (precategory_morphisms (to_BinDirectSums A (C1 i) (to_BinDirectSums A (C1 (i + 1)) (C2 i)))) (maponpaths (λ (i0 : hz), BinDirectSumOb (to_BinDirectSums A (C1 i0) (to_BinDirectSums A (C1 (i0 + 1)) (C2 i0)))) (hzrminusplus i 1)) (MappingCylinderIsoHomot f i · MappingCylinderDiff A f (i - 1))) = MappingCylinderIsoHomot_mor1 f i.
proof: Proof. cbn. rewrite transport_target_postcompose. unfold MappingCylinderIsoHomot. unfold MappingCylinderIsoHomot_mor1. cbn. set (DS1 := to_BinDirectSums A (C1 (i + 1)) (C2 i)). set (DS2 := to_BinDirectSums A (C1 i) DS1). set (DS3 := to_BinDirectSums A (C1 (i - 1 + 1)) (C2 (i - 1))). set (DS4 := to_BinDirectSums A (C1 (i - 1)) DS3). set (DS5 := to_BinDirectSums A (C1 (i - 1 + 1 + 1)) (C2 (i - 1 + 1))). set (DS6 := to_BinDirectSums A (C1 (i - 1 + 1)) DS5). cbn. rewrite <- assoc. rewrite <- assoc. rewrite <- to_premor_linear'. rewrite <- to_premor_linear'. apply cancel_precomposition. rewrite <- transport_target_postcompose. rewrite assoc. rewrite assoc. rewrite <- to_postmor_linear'. rewrite <- transport_target_postcompose. rewrite <- transport_source_precompose. unfold MappingCylinderDiff. unfold MappingCylinderDiff1. unfold MappingCylinderDiff2. unfold MappingCylinderDiff3. cbn. fold DS1 DS2 DS3 DS4 DS5 DS6. cbn. rewrite assoc. rewrite assoc. rewrite assoc. rewrite assoc. rewrite <- PreAdditive_invrcomp. rewrite <- PreAdditive_invrcomp. rewrite to_premor_linear'. rewrite assoc. rewrite assoc. rewrite <- PreAdditive_invlcomp. rewrite <- (assoc _ _ (to_Pr1 DS4)). rewrite (to_Unel2' DS4). rewrite ZeroArrow_comp_right. rewrite to_inv_zero. rewrite ZeroArrow_comp_left. rewrite ZeroArrow_comp_left. rewrite to_lunax''. rewrite to_premor_linear'. rewrite assoc. rewrite assoc. rewrite assoc. rewrite <- PreAdditive_invlcomp. rewrite <- PreAdditive_invrcomp. rewrite assoc. rewrite <- PreAdditive_invlcomp. rewrite <- PreAdditive_invlcomp. rewrite <- PreAdditive_invlcomp. rewrite <- PreAdditive_invlcomp. rewrite <- PreAdditive_invlcomp. rewrite <- (assoc _ _ (to_Pr2 DS4)). rewrite (to_IdIn2 DS4). rewrite id_right. rewrite inv_inv_eq. unfold MappingConeDiff. unfold MappingConeDiff1. unfold MappingConeDiff2. unfold MappingConeDiff3. cbn. fold DS1 DS2 DS3 DS4 DS5 DS6. cbn. rewrite to_premor_linear'. rewrite assoc. rewrite to_premor_linear'. rewrite assoc. rewrite assoc. rewrite assoc. rewrite assoc. rewrite assoc. rewrite (to_IdIn1 DS3). rewrite id_left. rewrite id_left. rewrite (to_Unel1' DS3). rewrite id_left. rewrite ZeroArrow_comp_left. rewrite ZeroArrow_comp_left. rewrite to_runax''. unfold DiffTranslationComplex. cbn. rewrite <- transport_source_to_binop. rewrite <- transport_target_to_binop. rewrite <- transport_source_to_inv. rewrite <- transport_target_to_inv. cbn. rewrite to_postmor_linear'. rewrite <- transport_source_to_binop. rewrite <- transport_target_to_binop. assert (e1 : (transportf (precategory_morphisms (C1 i)) (maponpaths (λ (i0 : pr1 hz), BinDirectSumOb (to_BinDirectSums A (C1 i0) (to_BinDirectSums A (C1 (i0 + 1)) (C2 i0)))) (hzrminusplus i 1)) (transportf (λ x' : A, A ⟦ x', DS6 ⟧) (maponpaths C1 (hzrminusplus i 1)) (to_In1 DS6))) = (to_In1 DS2)). { cbn. unfold DS2, DS1, DS6, DS5. set (tmp := λ (i0 : hz), BinDirectSumOb (to_BinDirectSums A (C1 i0) (to_BinDirectSums A (C1 (i0 + 1)) (C2 i0)))). set (tmp'' := (λ (i0 : hz), to_In1 (to_BinDirectSums A (C1 i0) (to_BinDirectSums A (C1 (i0 + 1)) (C2 i0))))). set (tmp' := @transport_hz_double_section_source_target A C1 tmp tmp'' _ _ (hzrminusplus i 1)). unfold tmp'' in tmp'. rewrite tmp'. unfold tmp. apply idpath. } cbn in e1. cbn. rewrite <- e1. clear e1. apply maponpaths. rewrite <- to_binop_inv_inv. rewrite transport_target_to_inv. rewrite transport_source_to_inv. rewrite <- PreAdditive_invlcomp. rewrite <- PreAdditive_invlcomp. rewrite inv_inv_eq. rewrite transport_target_to_inv. rewrite transport_source_to_inv. rewrite PreAdditive_invlcomp. rewrite PreAdditive_invlcomp. rewrite to_postmor_linear'. assert (e1 : (transportf (precategory_morphisms (C1 i)) (maponpaths (λ (i0 : pr1 hz), BinDirectSumOb (to_BinDirectSums A (C1 i0) (to_BinDirectSums A (C1 (i0 + 1)) (C2 i0)))) (hzrminusplus i 1)) (transportf (λ x' : A, A ⟦ x', DS6 ⟧) (maponpaths C1 (hzrminusplus i 1)) (Diff C1 (i - 1 + 1) · to_In1 DS5 · to_In2 DS6))) = (Diff C1 i · to_In1 DS1 · to_In2 DS2)). { cbn. unfold DS2, DS1, DS6, DS5. set (tmp := λ i0 : hz, BinDirectSumOb (to_BinDirectSums A (C1 i0) (to_BinDirectSums A (C1 (i0 + 1)) (C2 i0)))). set (tmp'' := (λ (i0 : hz), (Diff C1 i0) · (to_In1 (to_BinDirectSums A (C1 (i0 + 1)) (C2 i0))) · (to_In2 (to_BinDirectSums A (C1 i0) (to_BinDirectSums A (C1 (i0 + 1)) (C2 i0)))))). set (tmp' := @transport_hz_double_section_source_target A C1 tmp tmp'' _ _ (hzrminusplus i 1)). unfold tmp'' in tmp'. rewrite tmp'. unfold tmp. apply idpath. } rewrite <- e1. clear e1. apply maponpaths. cbn. unfold DS2, DS1, DS6, DS5. set (tmp := λ i0 : hz, BinDirectSumOb (to_BinDirectSums A (C1 i0) (to_BinDirectSums A (C1 (i0 + 1)) (C2 i0)))). set (tmp'' := (λ (i0 : hz), (to_inv (MMor f i0)) · (to_In2 (to_BinDirectSums A (C1 (i0 + 1)) (C2 i0))) · (to_In2 (to_BinDirectSums A (C1 i0) (to_BinDirectSums A (C1 (i0 + 1)) (C2 i0)))))). set (tmp' := @transport_hz_double_section_source_target A C1 tmp tmp'' _ _ (hzrminusplus i 1)). unfold tmp'' in tmp'. rewrite tmp'. unfold tmp. apply idpath. Qed.
imports: UniMath.Foundations.UnivalenceAxiom UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.Foundations.NaturalNumbers 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 UniMath.HomologicalAlgebra.MappingCone