Lemma IDMappingCone_is_z_isomorphism_inverses (C : Complex A) : is_inverse_in_precat (ZeroArrow (Additive.to_Zero (ComplexHomot_Additive A)) ((ComplexHomotFunctor A) (Additive.to_Zero (ComplexPreCat_Additive A))) ((ComplexHomotFunctor A) (MappingCone A (@identity (ComplexPreCat_Additive A) C)))) (ZeroArrow (Additive.to_Zero (ComplexHomot_Additive A)) ((ComplexHomotFunctor A) (MappingCone A (@identity (ComplexPreCat_Additive A) C))) ((ComplexHomotFunctor A) (Additive.to_Zero (ComplexPreCat_Additive A)))). Proof. use make_is_inverse_in_precat. - rewrite ZeroArrow_comp_left. use (@ArrowsToZero (ComplexHomot_Additive A) (Additive.to_Zero (ComplexHomot_Additive A))). - rewrite ZeroArrow_comp_left. use (pathscomp0 _ (functor_id (ComplexHomotFunctor A) (MappingCone A (@identity (ComplexPreCat_Additive A) C)))). use (pathscomp0 (! (AdditiveFunctorZeroArrow (ComplexHomotFunctor A) _ _))). exact (! (IDMappingConeEq C)). Qed.
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.MoreFoundations.PartA. Require Import UniMath.Algebra.BinaryOperations. Require Import UniMath.Algebra.Monoids. 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.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. 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. Require Import UniMath.HomologicalAlgebra.TranslationFunctors.