Definition CokernelKernelMorphism (C : Complex (AbelianToAdditive A)) (i : hz) : iscontr (∑ f : A⟦(CokernelComplex C) i, (KernelComplex C) i⟧, ((KernelIn (to_Zero A) (Kernel (Diff C (i + 1))) (C i) (Diff C i) (DSq _ C i)) = (transportf (λ (i0 : hz), A⟦C i0, (Cokernel (Diff C (i - 1)))⟧) (hzrminusplus i 1) (CokernelArrow (Cokernel (Diff C (i - 1))))) · f) × ((CokernelOut (to_Zero A) (Cokernel (Diff C (i - 1))) (C (i + 1)) (transportf (λ x : A, A ⟦ x, C (i + 1) ⟧) (! maponpaths C (hzrminusplus i 1)) (Diff C i)) (CokernelKernelMorphism_comm1' C i)) = f · (KernelArrow (Kernel (Diff C (i + 1)))))). Proof. use tpair. - use tpair. + cbn. use KernelIn. * use CokernelOut. -- exact (transportf (λ (x : A), A⟦x, C(i + 1)⟧) (! maponpaths C (hzrminusplus i 1)) (Diff C i)). -- exact (CokernelKernelMorphism_comm1 C i). * exact (CokernelKernelMorphism_comm2 C i). + cbn. split. * exact (CokernelKernelMorphism_comm3 C i). * exact (CokernelKernelMorphism_comm2' C i). - cbn. exact (CokernelKernelMorphism_uni 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.