Lemma CohomologyFunctorH_Mor_eq {C1 C2 : ComplexHomot_Additive (AbelianToAdditive A)} (f : ComplexHomot_Additive (AbelianToAdditive A) ⟦C1, C2⟧) (H : hfiber # (ComplexHomotFunctor (AbelianToAdditive A)) f) (f' : ComplexPreCat_Additive (AbelianToAdditive A) ⟦C1, C2⟧) (H' : # (ComplexHomotFunctor (AbelianToAdditive A)) f' = f) : # (CohomologyFunctor A) (pr1 H) = # (CohomologyFunctor A) f'. Proof. use CohomologyFunctorHomotopies. use (@abgrquotpr_rel_paths _ (binopeqrel_subgr_eqrel (ComplexHomotSubgrp (AbelianToAdditive A) C1 C2))). use (pathscomp0 (hfiberpr2 _ _ H)). apply pathsinv0. exact H'. 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.