Lemma TranslationInvTranslation_adjunction_eq1 (x : ob (ComplexPreCat_Additive A)) : (# TranslationFunctor_Additive (TranslationTranslationInvNatTrans x)) · (InvTranslationTranslationNatTrans (TranslationFunctor_Additive x)) = identity (TranslationFunctor_Additive x). Proof. use MorphismEq. intros i. cbn. rewrite <- transport_target_postcompose. rewrite id_right. rewrite transport_f_f. assert (e : maponpaths (λ i0 : pr1 hz, (x : Complex A) (i0 + 1)) (hzrplusminus i 1) = maponpaths (x : Complex A) (maponpaths (λ i0 : hz, (i0 + 1)) (hzrplusminus i 1))). { induction (hzrplusminus i 1). apply idpath. } rewrite e. clear e. rewrite <- maponpathscomp0. assert (e : ! hzrminusplus (i + 1) 1 @ maponpaths (λ i0 : hz, i0 + 1) (hzrplusminus i 1) = idpath _) by apply isasethz. cbn in e. cbn. rewrite e. clear e. apply idpath. 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.