Lemma TranslationFunctorHomotopies {C1 C2 : Complex A} (H : ComplexHomot A C1 C2) : ComplexHomotMorphism A (TranslationHomot H) = TranslationMorphism C1 C2 (ComplexHomotMorphism A H). 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.
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.Core.Univalence. 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.