proposition: Lemma MappingCylinderIsoHomot_eq {C1 C2 : Complex A} (f : (ComplexPreCat_Additive A)⟦C1, C2⟧) : to_binop _ _ (identity _) (to_inv (MappingCylinderMor2 f · MappingCylinderMor1 f)) = ComplexHomotMorphism A (MappingCylinderIsoHomot f).
proof: Proof. use MorphismEq. intros i. cbn. unfold MappingCylinderMor1_mor. unfold MappingCylinderMor2_mor. cbn. set (DS1 := to_BinDirectSums A (C1 (i + 1)) (C2 i)). set (DS2 := to_BinDirectSums A (C1 i) DS1). rewrite to_postmor_linear'. rewrite <- to_binop_inv_inv. rewrite <- (to_BinOpId DS2). assert (e : to_Pr2 DS2 · to_In2 DS2 = to_Pr2 DS2 · identity _ · to_In2 DS2). { rewrite id_right. apply idpath. } rewrite e. clear e. rewrite <- (to_BinOpId DS1). rewrite to_premor_linear'. rewrite to_postmor_linear'. rewrite assoc. rewrite assoc. rewrite assoc. rewrite assoc. rewrite to_assoc. rewrite to_assoc. rewrite (to_commax' _ (to_inv (to_Pr1 DS2 · MMor f i · to_In2 DS1 · to_In2 DS2))). rewrite <- (to_assoc _ _ _ (to_inv (to_Pr1 DS2 · MMor f i · to_In2 DS1 · to_In2 DS2))). rewrite (@to_rinvax' A (Additive.to_Zero A)). rewrite to_lunax''. rewrite <- to_assoc. use (pathscomp0 (MappingCylinderisoHomot_eq3 f i)). rewrite <- (MappingCylinderIsoHomot_eq1 f i). rewrite <- (MappyngCylinderIsoHomot_eq2 f i). unfold DS2. unfold DS1. apply idpath. Qed.
imports: UniMath.Foundations.UnivalenceAxiom UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.Foundations.NaturalNumbers 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 UniMath.HomologicalAlgebra.MappingCone