Definition CohomologyComplexIso_Mor8 (C : Complex (AbelianToAdditive A)) (i : hz) : let φ1 := KernelArrow (Kernel (Diff C i)) in let φ2 := CokernelArrow (Cokernel (transportf (precategory_morphisms (C (i - 1))) (maponpaths C (hzrminusplus i 1)) (Diff C (i - 1)))) in let CK4 := make_Cokernel _ _ _ (CohomologyComplexIso_isCokernel_Eq C i) (CohomologyComplexIso_isCokernel C i) in iso (Kernel (CokernelArrow CK4)) (Image (φ1 · φ2)) := let φ1 := KernelArrow (Kernel (Diff C i)) in let φ2 := CokernelArrow (Cokernel (transportf (precategory_morphisms (C (i - 1))) (maponpaths C (hzrminusplus i 1)) (Diff C (i - 1)))) in let CK4 := make_Cokernel _ _ _ (CohomologyComplexIso_isCokernel_Eq C i) (CohomologyComplexIso_isCokernel C i) in CohomologyComplexIso_KerCokerIso CK4 _ (Kernel (CokernelArrow CK4)) (Image (φ1 · φ2)).
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.