Lemma TranslationHInvTranslationH : functor_composite TranslationFunctorH InvTranslationFunctorH = 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 (hzrminusplus i 1). * intros i. cbn. exact (TranslationInvTranslation_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 (TranslationFunctorH_Mor_unique _ f'). use (squash_to_prop (ComplexHomotFunctor_issurj A (TranslationFunctorHImMor (TranslationFunctorH_Mor_data f f')))). { use (@to_has_homsets (ComplexHomot_Additive A)). } intros f''. rewrite (InvTranslationFunctorH_Mor_unique _ f''). rewrite <- (hfiberpr2 _ _ f'). rewrite <- (TranslationInvTranslation_eq2 (hfiberpr1 # (ComplexHomotFunctor A) f f')). rewrite transport_target_ComplexHomotFunctor. rewrite transport_source_ComplexHomotFunctor. apply maponpaths. apply maponpaths. assert (e1 : # (ComplexHomotFunctor A) (InvTranslationMorphism (TranslationComplex C1) (TranslationComplex C2) (TranslationMorphism C1 C2 (hfiberpr1 # (ComplexHomotFunctor A) f f'))) = # InvTranslationFunctorH (# (ComplexHomotFunctor A) (TranslationMorphism C1 C2 (hfiberpr1 # (ComplexHomotFunctor A) f f')))). { apply pathsinv0. use InvTranslationFunctorHImEq. apply idpath. } use (pathscomp0 _ (! e1)). clear e1. apply pathsinv0. use InvTranslationFunctorHImEq. set (tmp := hfiberpr2 _ _ f''). rewrite tmp. clear tmp. use TranslationFunctorHImEq. 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.