proposition: Lemma TranslationFunctorHomotopies {C1 C2 : Complex A} (H : ComplexHomot A C1 C2) : ComplexHomotMorphism A (TranslationHomot H) = TranslationMorphism C1 C2 (ComplexHomotMorphism A H).
proof: Proof. unfold TranslationHomot. cbn. use MorphismEq. intros i. cbn. induction (hzrminusplus i 1). cbn. rewrite pathscomp0rid. cbn. rewrite <- PreAdditive_invrcomp. rewrite <- transport_target_to_inv. rewrite PreAdditive_invlcomp. rewrite inv_inv_eq. rewrite <- transport_target_to_inv. rewrite <- PreAdditive_invlcomp. rewrite <- PreAdditive_invrcomp. rewrite inv_inv_eq. assert (e : (maponpaths (λ i0 : pr1 hz, C2 (i0 + 1)) (hzrplusminus (i - 1 + 1) 1)) = (maponpaths C2 (maponpaths (λ (i0 : hz), i0 + 1) (hzrplusminus (i - 1 + 1) 1)))). { induction (hzrplusminus (i - 1 + 1) 1). apply idpath. } cbn in e. rewrite e. clear e. assert (e1 : (transportf (precategory_morphisms (C1 (i - 1 + 1 + 1))) (maponpaths C2 (maponpaths (λ i0 : pr1 hz, i0 + 1) (hzrplusminus (i - 1 + 1) 1))) ((Diff C1 (i - 1 + 1 + 1)) · (transportf (precategory_morphisms (C1 (i - 1 + 1 + 1 + 1))) (maponpaths C2 (hzrplusminus (i - 1 + 1 + 1) 1 @ ! hzrminusplus (i - 1 + 1 + 1) 1)) (H (i - 1 + 1 + 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_f_f. rewrite <- maponpathscomp0. set (tmp := ((hzrplusminus (i - 1 + 1 + 1) 1 @ ! hzrminusplus (i - 1 + 1 + 1) 1) @ maponpaths (λ i0 : pr1 hz, i0 + 1) (hzrplusminus (i - 1 + 1) 1))). assert (ee : tmp = (hzrplusminus (i - 1 + 1 + 1) 1)) by apply isasethz. unfold tmp in ee. cbn in ee. unfold tmp. cbn. rewrite ee. clear ee. clear tmp. induction (hzrplusminus (i - 1 + 1 + 1) 1). cbn. apply idpath. } cbn in e1. rewrite e1. clear e1. use maponpaths_2. set (tmp := @transport_hz_source_target A C2 1 (Diff C2) _ _ (hzrplusminus (i - 1 + 1) 1)). rewrite tmp. clear tmp. rewrite transport_compose. rewrite transport_target_postcompose. apply cancel_precomposition. rewrite transport_f_f. rewrite <- maponpathsinv0. rewrite <- maponpathscomp0. rewrite pathsinv0r. rewrite <- functtransportf. rewrite idpath_transportf. apply 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