proposition: Lemma InvTranslationFunctorHomotopies {C1 C2 : Complex A} (H : ComplexHomot A C1 C2) : ComplexHomotMorphism A (InvTranslationHomot H) = InvTranslationMorphism C1 C2 (ComplexHomotMorphism A H).
proof: Proof. unfold InvTranslationHomot. cbn. use MorphismEq. intros i. cbn. induction (hzrplusminus i 1). cbn. rewrite pathscomp0rid. rewrite <- transport_target_to_inv. rewrite <- PreAdditive_invrcomp. rewrite <- PreAdditive_invlcomp. rewrite inv_inv_eq. rewrite <- transport_target_to_inv. rewrite <- PreAdditive_invlcomp. rewrite <- PreAdditive_invrcomp. rewrite inv_inv_eq. assert (e1 : transportf (precategory_morphisms (C1 (i + 1 - 1 - 1))) (maponpaths C1 (hzrminusplus (i + 1 - 1) 1)) (Diff C1 (i + 1 - 1 - 1)) · H (i + 1 - 1) = transportf (precategory_morphisms (C1 (i + 1 - 1 - 1))) (maponpaths C2 (hzrplusminus (i + 1 - 1 - 1) 1)) (Diff C1 (i + 1 - 1 - 1) · H (i + 1 - 1 - 1 + 1))). { rewrite transport_target_postcompose. rewrite transport_compose. apply cancel_precomposition. rewrite <- maponpathsinv0. rewrite <- (transport_hz_double_section A _ _ H _ _ (hzrminusplus (i + 1 - 1) 1)). use transportf_paths. assert (e2 : maponpaths (λ i0 : hz, C2 (i0 - 1)) (hzrminusplus (i + 1 - 1) 1) = maponpaths C2 (maponpaths (λ i0 : hz, i0 - 1) (hzrminusplus (i + 1 - 1) 1))). { induction (hzrminusplus (i + 1 - 1) 1). apply idpath. } rewrite e2. clear e2. apply maponpaths. apply isasethz. } cbn in e1. rewrite e1. clear e1. use maponpaths_2. rewrite <- transport_target_postcompose. rewrite transport_f_f. assert (e2 : maponpaths (λ i0 : pr1 hz, C2 (i0 - 1)) (hzrminusplus (i + 1 - 1) 1) = maponpaths C2 (maponpaths (λ i0 : hz, i0 - 1) (hzrminusplus (i + 1 - 1) 1))). { induction (hzrminusplus (i + 1 - 1) 1). apply idpath. } rewrite e2. clear e2. rewrite <- maponpathscomp0. use transportf_paths. apply maponpaths. apply isasethz. 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.Core.Univalence 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