Lemma InvTranslationFunctorH_comm : functor_composite (ComplexHomotFunctor A) InvTranslationFunctorH = functor_composite InvTranslationFunctor (ComplexHomotFunctor A). Proof. use functor_eq. - apply to_has_homsets. - use functor_data_eq. + intros C. cbn. apply idpath. + intros C1 C2 f. unfold double_transport. rewrite idpath_transportf. rewrite idpath_transportf. assert (e1 : pr2 (pr1 (functor_composite (ComplexHomotFunctor A) InvTranslationFunctorH)) C1 C2 f = # InvTranslationFunctorH (# (ComplexHomotFunctor A) f)) by apply idpath. rewrite e1. clear e1. assert (e2 : pr2 (pr1 (functor_composite InvTranslationFunctor (ComplexHomotFunctor A))) C1 C2 f = # (ComplexHomotFunctor A) (# InvTranslationFunctor f)) by apply idpath. rewrite e2. clear e2. use (squash_to_prop (ComplexHomotFunctor_issurj A (# (ComplexHomotFunctor A) f))). { apply to_has_homsets. } intros f'. set (im := InvTranslationFunctorH_Mor_data (# (ComplexHomotFunctor A) f) f'). rewrite <- (@InvTranslationFunctorHImEq C1 C2 _ im f (idpath _)). use InvTranslationFunctorHImEq. exact (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.