Lemma InvTranslationFunctorHomotopies {C1 C2 : Complex A} (H : ComplexHomot A C1 C2) : ComplexHomotMorphism A (InvTranslationHomot H) = InvTranslationMorphism C1 C2 (ComplexHomotMorphism A H). 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.
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.