Lemma TranslationInvTranslation_adjunction_eq2 (x : ob (ComplexPreCat_Additive A)) : (TranslationTranslationInvNatTrans (InvTranslationFunctor_Additive x)) · (# InvTranslationFunctor_Additive (InvTranslationTranslationNatTrans x)) = identity (InvTranslationFunctor_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)) (! hzrminusplus i 1) @ maponpaths (x : Complex A) (hzrplusminus (i - 1) 1) = idpath _). { assert (e1 : maponpaths (λ i0 : pr1 hz, (x : Complex A) (i0 - 1)) (! hzrminusplus i 1) = maponpaths (x : Complex A) (maponpaths (λ i0 : hz, (i0 - 1)) (! hzrminusplus i 1))). { induction (hzrminusplus i 1). apply idpath. } rewrite e1. rewrite <- maponpathscomp0. clear e1. assert (e2 : maponpaths (λ i0 : hz, i0 - 1) (! hzrminusplus i 1) @ hzrplusminus (i - 1) 1 = idpath _) by apply isasethz. rewrite e2. apply idpath. } cbn. cbn in e. 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.