Lemma CohomologyFunctorHomotopy {C1 C2 : Complex (AbelianToAdditive A)} (H : ComplexHomot _ C1 C2) : CohomologyMorphism A (ComplexHomotMorphism (AbelianToAdditive A) H) = ZeroMorphism (AbelianToAdditive A) (CohomologyComplex A C1) (CohomologyComplex A C2). Proof. use MorphismEq. intros i. cbn. unfold CohomologyMorphism_Mor. use CokernelOutsEq. rewrite CokernelCommutes. rewrite ZeroArrow_comp_right. set (tmp := @KernelIn _ (to_Zero A) _ _ _ (Kernel (Diff C2 i)) (Kernel (Diff C1 i)) (KernelArrow (Kernel (Diff C1 i)) · (transportf (precategory_morphisms (C1 i)) (maponpaths C2 (hzrminusplus i 1)) (H i · Diff C2 (i - 1)))) (CohomologyFunctorHomotopy_eq1 H i)). assert (e0 : KernelIn (to_Zero A) (Kernel (Diff C2 i)) (Kernel (Diff C1 i)) (KernelArrow (Kernel (Diff C1 i)) · Abelian_op A (C1 i) (C2 i) (transportf (precategory_morphisms (C1 i)) (maponpaths C2 (hzrminusplus i 1)) (H i · Diff C2 (i - 1))) (transportf (precategory_morphisms (C1 i)) (maponpaths C2 (hzrplusminus i 1)) (Diff C1 i · H (i + 1)))) (CohomologyMorphism_KernelIn_comm A (ComplexHomotMorphism (AbelianToAdditive A) H) i) = tmp). { unfold tmp. clear tmp. use KernelInsEq. rewrite KernelCommutes. rewrite KernelCommutes. set (tmp := @to_premor_linear' (AbelianToAdditive A)). cbn in tmp. rewrite tmp. clear tmp. rewrite transport_target_postcompose. rewrite transport_target_postcompose. rewrite assoc. rewrite assoc. rewrite KernelCompZero. rewrite ZeroArrow_comp_left. rewrite <- PreAdditive_unel_zero. set (tmp := @to_runax' (AbelianToAdditive A)). cbn in tmp. rewrite tmp. clear tmp. apply idpath. } cbn. cbn in e0. rewrite e0. clear e0. unfold tmp. clear tmp. assert (e1 : KernelIn (to_Zero A) (Kernel (Diff C2 i)) (Kernel (Diff C1 i)) ((KernelArrow (Kernel (Diff C1 i))) · (transportf (precategory_morphisms (C1 i)) (maponpaths C2 (hzrminusplus i 1)) (H i · Diff C2 (i - 1)))) (CohomologyFunctorHomotopy_eq1 H i) = (KernelArrow (Kernel (Diff C1 i))) · (H i) · (KernelIn ((to_Zero A)) (Abelian.Kernel (Diff C2 i)) _ _ (CohomologyComplex_KernelIn_eq A C2 i))). { use KernelInsEq. rewrite KernelCommutes. rewrite <- assoc. rewrite <- assoc. apply cancel_precomposition. rewrite KernelCommutes. rewrite transport_target_postcompose. apply idpath. } cbn. cbn in e1. rewrite e1. clear e1. rewrite <- assoc. rewrite CokernelCompZero. rewrite ZeroArrow_comp_right. apply idpath. 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.