Lemma InvTranslationFunctorPreservesHomotopies {C1 C2 : Complex A} (f g : (ComplexPreCat_Additive A)⟦C1, C2⟧) (H : subgrhrel (ComplexHomotSubgrp A C1 C2) f g) : subgrhrel (ComplexHomotSubgrp A _ _) (InvTranslationMorphism C1 C2 f) (InvTranslationMorphism C1 C2 g). Proof. use (squash_to_prop H). { apply propproperty. } intros H'. clear H. induction H' as [H1 H2]. induction H1 as [H11 H12]. cbn in H11. use (squash_to_prop H12). { apply propproperty. } intros H. cbn in H2. induction H as [HH1 HH2]. intros P X. apply X. clear X P. use tpair. - use tpair. + cbn. exact (InvTranslationMorphism _ _ H11). + intros P X. apply X. clear X P. use tpair. * exact (InvTranslationHomot HH1). * cbn. rewrite InvTranslationFunctorHomotopies. rewrite HH2. apply idpath. - cbn. rewrite H2. set (tmp := @AdditiveFunctorLinear (ComplexPreCat_Additive A) (ComplexPreCat_Additive A) InvTranslationFunctor_Additive C1 C2 f (to_inv g)). cbn in tmp. rewrite tmp. clear tmp. apply maponpaths. set (tmp := @AdditiveFunctorInv (ComplexPreCat_Additive A) (ComplexPreCat_Additive A) InvTranslationFunctor_Additive C1 C2 g). cbn in tmp. exact tmp. 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.