Definition CokernelKernelCohomology1_Mor1 (C : Complex (AbelianToAdditive A)) (i : hz) : A⟦(((CohomologyFunctor A C) : Complex (AbelianToAdditive A)) i), (Kernel (pr1 (pr1 (CokernelKernelMorphism C i))))⟧. Proof. set (K := Kernel (CokernelOut (to_Zero A) (Cokernel (transportf (precategory_morphisms (C (i - 1))) (maponpaths C (hzrminusplus i 1)) (Diff C (i - 1)))) (C (i + 1)) (Diff C i) (CohomologyComplex_KernelIn_eq A C i))). use (compose (iso_inv_from_is_iso _ (CohomologyComplexIso_is_iso_i A C i))). use KernelIn. - cbn. use (compose (KernelArrow K)). use CokernelOut. + exact (transportf (λ x' : A, A ⟦x', Cokernel (Diff C (i - 1))⟧) (maponpaths C (hzrminusplus i 1)) (CokernelArrow (Cokernel (Diff C (i - 1))))). + exact (CokernelKernelCohomology1_Mor1_eq1 C i). - exact (CokernelKernelCohomology1_Mor1_comm1 C i). Defined.
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.