Definition CohomologyComplexIso_Mor_i (C : Complex (AbelianToAdditive A)) (i : hz) : AbelianToAdditive A ⟦((CohomologyComplex' C) : Complex (AbelianToAdditive A)) i, ((CohomologyComplex A C) : Complex (AbelianToAdditive A)) i⟧. Proof. cbn. set (φ1 := KernelArrow (Kernel (Diff C i))). set (φ2 := CokernelArrow (Cokernel (transportf (precategory_morphisms (C (i - 1))) (maponpaths C (hzrminusplus i 1)) (Diff C (i - 1))))). set (f1 := factorization1 (transportf (precategory_morphisms (C (i - 1))) (maponpaths C (hzrminusplus i 1)) (Diff C (i - 1)))). set (f2 := factorization2 (Diff C i)). set (K1 := KernelIn (to_Zero A) (Kernel (Diff C i)) _ _ (CohomologyComplexIso_eq1 C i)). set (CK1 := CokernelOut (to_Zero A) (Cokernel (transportf (precategory_morphisms (C (i - 1))) (maponpaths C (hzrminusplus i 1)) (Diff C (i - 1)))) _ _ (CohomologyComplexIso_eq2 C i)). use (postcompose (CohomologyComplexIso_Mor1 C i)). use (postcompose (CohomologyComplexIso_Mor2 C i)). use (compose (CohomologyComplexIso_Mor3 C i)). use (compose (CohomologyComplexIso_Mor4 C i)). set (CK2 := CokernelPath A (to_Zero A) f1 (Cokernel _)). set (CK2' := CokernelEpiComp A (to_Zero A) _ _ CK2). set (K3 := MonicToKernel' A _ CK2'). set (K4 := make_Kernel _ _ _ (CohomologyComplexIso_isKernel_Eq C i) (CohomologyComplexIso_isKernel C i)). use (postcompose (CohomologyComplexIso_Mor5 C i)). use (postcompose (CohomologyComplexIso_Mor6 C i)). set (K2 := KernelPath A (to_Zero A) f2 (Kernel _)). set (K2' := KernelCompMonic A (to_Zero A) _ _ K2). set (CK3 := EpiToCokernel' A _ K2'). set (CK4 := make_Cokernel _ _ _ (CohomologyComplexIso_isCokernel_Eq C i) (CohomologyComplexIso_isCokernel C i)). use (compose (CohomologyComplexIso_Mor7 C i)). use (compose (CohomologyComplexIso_Mor8 C i)). exact (iso_inv_from_is_iso _ (is_iso_qinv _ _ (CoIm_to_Im_is_iso A (φ1 · φ2)))). 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.