proposition: 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: 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.
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