proposition: Lemma CohomologyFunctorHomotopies {C1 C2 : Complex (AbelianToAdditive A)} (f g : (ComplexPreCat_Additive (AbelianToAdditive A))⟦C1, C2⟧) (H : subgrhrel (ComplexHomotSubgrp (AbelianToAdditive A) C1 C2) f g) : # (CohomologyFunctor_Additive A) f = # (CohomologyFunctor_Additive A) g.
proof: Proof. set (inv := @to_inv (ComplexPreCat_Additive (AbelianToAdditive A)) _ _ (# (CohomologyFunctor_Additive A) g)). set (tmp := @grrcan (@to_abgr (ComplexPreCat_Additive (AbelianToAdditive A)) _ _) (# (CohomologyFunctor_Additive A) f) (# (CohomologyFunctor_Additive A) g) inv). apply tmp. clear tmp. unfold inv. clear inv. set (tmp := @rinvax (ComplexPreCat_Additive (AbelianToAdditive A)) _ _ (# (CohomologyFunctor_Additive A) g)). use (pathscomp0 _ (! tmp)). clear tmp. rewrite <- AdditiveFunctorInv. set (tmp := AdditiveFunctorLinear (CohomologyFunctor_Additive A) f (to_inv g)). apply pathsinv0 in tmp. use (pathscomp0 tmp). clear tmp. use (squash_to_prop H). { apply has_homsets_ComplexPreCat_AbelianPreCat. } intros H'. induction H' as [H1 H2]. induction H1 as [H11 H12]. cbn in H11. cbn in H2. cbn. rewrite <- H2. clear H. use (squash_to_prop H12). { apply has_homsets_ComplexPreCat_AbelianPreCat. } intros G. induction G as [G1 G2]. rewrite <- G2. clear H11 H12 H2 G2. apply CohomologyFunctorHomotopy. Qed.
imports: UniMath.Foundations.UnivalenceAxiom UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.Foundations.NaturalNumbers UniMath.Algebra.BinaryOperations UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.NumberSystems.Integers UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.TransportMorphisms 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.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