proposition: 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: 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.
imports: UniMath.Foundations.UnivalenceAxiom UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.PartA UniMath.Algebra.BinaryOperations UniMath.Algebra.Monoids UniMath.NumberSystems.Integers UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.TransportMorphisms UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Limits.Zero UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Equalizers UniMath.CategoryTheory.Limits.Coequalizers UniMath.CategoryTheory.Limits.Kernels UniMath.CategoryTheory.Limits.Cokernels UniMath.CategoryTheory.Limits.Pushouts UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.Limits.BinDirectSums UniMath.CategoryTheory.Monics UniMath.CategoryTheory.Epis UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Equivalences.Core UniMath.CategoryTheory.CategoriesWithBinOps UniMath.CategoryTheory.PrecategoriesWithAbgrops UniMath.CategoryTheory.PreAdditive UniMath.CategoryTheory.Additive UniMath.CategoryTheory.Abelian UniMath.CategoryTheory.AbelianToAdditive UniMath.CategoryTheory.AdditiveFunctors UniMath.HomologicalAlgebra.Complexes UniMath.HomologicalAlgebra.KA