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. 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.
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.Algebra.BinaryOperations. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups. 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.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.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.