Lemma InvTranslationHTranslationH : functor_composite InvTranslationFunctorH TranslationFunctorH = functor_identity _. Proof. use functor_eq. - apply to_has_homsets. - use functor_data_eq. + intros C. cbn. use ComplexEq. * intros i. cbn. apply maponpaths. apply (hzrplusminus i 1). * intros i. cbn. exact (InvTranslationTranslation_eq1 C i). + intros C1 C2 f. unfold double_transport. use (squash_to_prop (ComplexHomotFunctor_issurj A f)). { use to_has_homsets. } intros f'. cbn. rewrite (InvTranslationFunctorH_Mor_unique _ f'). use (squash_to_prop (ComplexHomotFunctor_issurj A (InvTranslationFunctorHImMor (InvTranslationFunctorH_Mor_data f f')))). { use (@to_has_homsets (ComplexHomot_Additive A)). } intros f''. rewrite (TranslationFunctorH_Mor_unique _ f''). rewrite <- (hfiberpr2 _ _ f'). rewrite <- (InvTranslationTranslation_eq2 (hfiberpr1 # (ComplexHomotFunctor A) f f')). rewrite transport_target_ComplexHomotFunctor. rewrite transport_source_ComplexHomotFunctor. apply maponpaths. apply maponpaths. assert (e1 : # (ComplexHomotFunctor A) (TranslationMorphism (InvTranslationComplex C1) (InvTranslationComplex C2) (InvTranslationMorphism C1 C2 (hfiberpr1 # (ComplexHomotFunctor A) f f'))) = # TranslationFunctorH (# (ComplexHomotFunctor A) (InvTranslationMorphism C1 C2 (hfiberpr1 # (ComplexHomotFunctor A) f f')))). { apply pathsinv0. use TranslationFunctorHImEq. apply idpath. } use (pathscomp0 _ (! e1)). clear e1. apply pathsinv0. use TranslationFunctorHImEq. set (tmp := hfiberpr2 _ _ f''). rewrite tmp. clear tmp. use InvTranslationFunctorHImEq. apply (hfiberpr2 _ _ f'). 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.