Lemma TranslationHInvTranslationH_adjunction_eq2 (x : ComplexHomot_Additive A) : # (ComplexHomotFunctor A) (TranslationTranslationInvNatTrans_Mor (InvTranslationFunctorH x)) · # InvTranslationFunctorH (# (ComplexHomotFunctor A) (InvTranslationTranslationNatTrans_Mor x)) = identity (InvTranslationFunctorH x). Proof. use (pathscomp0 _ (functor_id InvTranslationFunctorH_AdditiveFunctor x)). set (tmp := functor_id (ComplexHomotFunctor A) x). apply (maponpaths (# InvTranslationFunctorH_AdditiveFunctor)) in tmp. use (pathscomp0 _ tmp). clear tmp. set (f' := @make_hfiber _ _ (# (ComplexHomotFunctor A)) (# (ComplexHomotFunctor A) (InvTranslationTranslationNatTrans_Mor x)) (InvTranslationTranslationNatTrans_Mor x) (idpath _)). set (tmp := InvTranslationFunctorH_Mor_Im _ f'). apply (maponpaths (compose (# (ComplexHomotFunctor A) (TranslationTranslationInvNatTrans_Mor (InvTranslationFunctorH x))))) in tmp. use (pathscomp0 tmp). clear tmp. set (id' := @make_hfiber _ _ (# (ComplexHomotFunctor A)) (# (ComplexHomotFunctor A) (identity _)) (identity (x : ob (ComplexPreCat_Additive A))) (idpath _)). set (tmp := InvTranslationFunctorH_Mor_Im _ id'). use (pathscomp0 _ (! tmp)). clear tmp. cbn. clear id'. set (tmp := functor_comp (ComplexHomotFunctor A) (TranslationTranslationInvNatTrans_Mor (InvTranslationFunctorH x)) (# InvTranslationFunctor (InvTranslationTranslationNatTrans_Mor x))). use (pathscomp0 (! tmp)). clear tmp. apply maponpaths. Local Transparent InvTranslationFunctorH. cbn. set (tmp := TranslationInvTranslation_adjunction_eq2 x). cbn in tmp. use (pathscomp0 tmp). clear tmp. apply pathsinv0. use (functor_id InvTranslationFunctor). 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.