proposition: Lemma MappingConePr1Eq (C : Complex A) : # (ComplexHomotFunctor A) (MappingConePr1 A (@identity (ComplexPreCat_Additive A) C)) = # (ComplexHomotFunctor A) (ZeroArrow (Additive.to_Zero (ComplexPreCat_Additive A)) _ _).
proof: Proof. use ComplexHomotFunctor_rel_mor'. - exact (MappingConePr1Homot C). - rewrite to_inv_zero. rewrite to_runax''. use MorphismEq. intros i. cbn. unfold MappingConePr1Homot. unfold MappingConeDiff. unfold MappingConeDiff1, MappingConeDiff2, MappingConeDiff3. cbn. set (DS1 := to_BinDirectSums A (C (i + 1)) (C i)). set (DS2 := to_BinDirectSums A (C (i + 1 + 1)) (C (i + 1))). rewrite id_left. rewrite to_postmor_linear'. rewrite to_postmor_linear'. rewrite <- transport_target_postcompose. rewrite <- transport_target_postcompose. rewrite <- transport_target_postcompose. rewrite assoc. rewrite assoc. rewrite <- assoc. rewrite <- assoc. rewrite <- assoc. rewrite <- assoc. rewrite (to_IdIn2 DS2). rewrite id_right. rewrite id_right. rewrite (to_Unel1' DS2). rewrite ZeroArrow_comp_right. rewrite ZeroArrow_comp_right. rewrite transport_target_ZeroArrow. rewrite (to_lunax''). assert (e1 : (transportf (precategory_morphisms DS1) (maponpaths (λ i0 : pr1 hz, C (i0 + 1)) (hzrplusminus i 1)) (to_binop DS1 (C (i + 1 - 1 + 1)) (transportf (precategory_morphisms DS1) (maponpaths C (! hzrminusplus (i + 1) 1)) (to_Pr1 DS1)) (transportf (precategory_morphisms DS1) (maponpaths C (! hzrminusplus (i + 1) 1)) (to_Pr2 DS1 · Diff C i)))) = to_binop DS1 (C (i + 1)) (to_Pr1 DS1) (to_Pr2 DS1 · Diff C i)). { unfold DS1, DS2. set (tmp := transport_hz_double_section_source_target A (λ (i0 : hz), to_BinDirectSums A (C (i0 + 1)) (C i0)) (λ i0 : hz, C (i0 + 1)) (λ (i0 : hz), to_binop (to_BinDirectSums A (C (i0 + 1)) (C i0)) (C (i0 + 1)) (to_Pr1 (to_BinDirectSums A (C (i0 + 1)) (C i0))) (to_Pr2 (to_BinDirectSums A (C (i0 + 1)) (C i0)) · Diff C i0)) _ _ (hzrplusminus i 1)). cbn beta in tmp. use (pathscomp0 _ (! tmp)). clear tmp. apply maponpaths. rewrite transport_target_to_binop. set (tmp := transport_hz_double_section A (λ i0 : hz, to_BinDirectSums A (C (i0 + 1)) (C i0)) (λ (i0 : hz), C (i0 + 1)) (λ i0 : hz, (to_binop (to_BinDirectSums A (C (i0 + 1)) (C i0)) (C (i0 + 1)) (to_Pr1 (to_BinDirectSums A (C (i0 + 1)) (C i0))) (to_Pr2 (to_BinDirectSums A (C (i0 + 1)) (C i0)) · Diff C i0))) _ _ (! hzrplusminus i 1)). cbn beta in tmp. assert (e2 : (maponpaths (λ i0 : hz, C (i0 + 1)) (! hzrplusminus i 1)) = (maponpaths C (! hzrminusplus (i + 1) 1))). { assert (e3 : maponpaths (λ i0 : hz, C (i0 + 1)) (! hzrplusminus i 1) = maponpaths C (maponpaths (λ (i0 : hz), i0 + 1) (! hzrplusminus i 1))). { induction (hzrplusminus i 1). apply idpath. } rewrite e3. clear e3. apply maponpaths. apply isasethz. } rewrite e2 in tmp. clear e2. use (pathscomp0 tmp). clear tmp. assert (e4 : (maponpaths (λ i0 : hz, BinDirectSumOb (to_BinDirectSums A (C (i0 + 1)) (C i0))) (! (! hzrplusminus i 1))) = (maponpaths (λ i0 : hz, BinDirectSumOb (to_BinDirectSums A (C (i0 + 1)) (C i0))) (hzrplusminus i 1))). { apply maponpaths. apply isasethz. } rewrite e4. apply idpath. } apply (maponpaths (λ gg : _, to_binop _ _ (transportf (precategory_morphisms DS1) (maponpaths (λ i0 : pr1 hz, C (i0 + 1)) (hzrminusplus i 1)) (transportf (precategory_morphisms DS1) (maponpaths C (! hzrminusplus i 1)) (to_Pr2 DS1) · to_inv (Diff C (i - 1 + 1)))) gg)) in e1. use (pathscomp0 _ (! e1)). clear e1. assert (e2 : (transportf (precategory_morphisms DS1) (maponpaths (λ i0 : pr1 hz, C (i0 + 1)) (hzrminusplus i 1)) (transportf (precategory_morphisms DS1) (maponpaths C (! hzrminusplus i 1)) (to_Pr2 DS1) · to_inv (Diff C (i - 1 + 1)))) = to_Pr2 DS1 · to_inv (Diff C i)). { rewrite transport_target_postcompose. rewrite transport_compose. apply cancel_precomposition. rewrite <- transport_target_to_inv. rewrite <- transport_source_to_inv. apply maponpaths. rewrite <- maponpathsinv0. rewrite pathsinv0inv0. induction (hzrminusplus i 1). apply idpath. } apply (maponpaths (λ gg : _, to_binop _ _ gg (to_binop DS1 (C (i + 1)) (to_Pr1 DS1) (to_Pr2 DS1 · Diff C i)))) in e2. use (pathscomp0 _ (! e2)). clear e2. rewrite to_commax'. rewrite to_assoc. rewrite <- to_premor_linear'. rewrite (@to_rinvax' A (Additive.to_Zero A)). rewrite ZeroArrow_comp_right. rewrite to_runax''. apply idpath. Qed.
imports: UniMath.Foundations.UnivalenceAxiom UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.PartA UniMath.Algebra.BinaryOperations UniMath.Algebra.Monoids UniMath.NumberSystems.Integers UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.TransportMorphisms UniMath.CategoryTheory.Limits.Zero UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Equalizers UniMath.CategoryTheory.Limits.Coequalizers UniMath.CategoryTheory.Limits.Kernels UniMath.CategoryTheory.Limits.Cokernels UniMath.CategoryTheory.Limits.Pushouts UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.Limits.BinDirectSums UniMath.CategoryTheory.Monics UniMath.CategoryTheory.Epis UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Equivalences.Core UniMath.CategoryTheory.CategoriesWithBinOps UniMath.CategoryTheory.PrecategoriesWithAbgrops UniMath.CategoryTheory.PreAdditive UniMath.CategoryTheory.Additive UniMath.CategoryTheory.Abelian UniMath.CategoryTheory.AbelianToAdditive UniMath.CategoryTheory.AdditiveFunctors UniMath.HomologicalAlgebra.Complexes UniMath.HomologicalAlgebra.KA UniMath.HomologicalAlgebra.TranslationFunctors