Definition RotMorphismCommMor1 {C1 C2 : Complex A} (f : Morphism C1 C2) (i : hz) : A⟦ (MappingCone A f) i, to_BinDirectSums A (TranslationComplex A C2 (i - 1 + 1)) ((MappingCone A f) (i - 1 + 1)) ⟧. Proof. cbn. use to_binop. - use compose. + exact (C2 i). + exact (to_Pr2 (to_BinDirectSums A (C1 (i + 1)) (C2 i))). + use compose. * exact (C2 (i + 1)). * exact (to_inv (Diff C2 i)). * exact (transportf (λ x' : ob A, precategory_morphisms x' (to_BinDirectSums A (C2 (i - 1 + 1 + 1)) (to_BinDirectSums A (C1 (i - 1 + 1 + 1)) (C2 (i - 1 + 1))))) (maponpaths C2 (maponpaths (λ i0 : hz, (i0 + 1)) (hzrminusplus i 1))) (to_In1 (to_BinDirectSums A (C2 (i - 1 + 1 + 1)) (to_BinDirectSums A (C1 (i - 1 + 1 + 1)) (C2 (i - 1 + 1)))))). - use compose. + exact (C2 i). + exact (to_Pr2 (to_BinDirectSums A (C1 (i + 1)) (C2 i))). + use compose. * exact (to_BinDirectSums A (C1 (i - 1 + 1 + 1)) (C2 (i - 1 + 1))). * exact (transportf (λ x' : ob A, precategory_morphisms x' (to_BinDirectSums A (C1 (i - 1 + 1 + 1)) (C2 (i - 1 + 1)))) (maponpaths C2 (hzrminusplus i 1)) (to_In2 (to_BinDirectSums A (C1 (i - 1 + 1 + 1)) (C2 (i - 1 + 1))))). * exact (to_In2 (to_BinDirectSums A (C2 (i - 1 + 1 + 1)) (to_BinDirectSums A (C1 (i - 1 + 1 + 1)) (C2 (i - 1 + 1))))). 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.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.