Definition MappingConeMorExtMor {C1 C1' C2 C2' : Complex A} (f : Morphism C1 C2) (f' : Morphism C1' C2') (g1 : Morphism C1 C1') (g2 : Morphism C2 C2') (H : ComplexHomot A C1 C2') (i : hz) : A ⟦ (MappingCone A f) i, (MappingCone A f') i ⟧. Proof. cbn. use to_binop. - use compose. + exact (C1 (i + 1)). + exact (to_Pr1 (to_BinDirectSums A (C1 (i + 1)) (C2 i))). + use compose. * exact (C1' (i + 1)). * exact (g1 (i + 1)). * exact (to_In1 (to_BinDirectSums A (C1' (i + 1)) (C2' i))). - use to_binop. + use compose. * exact (C1 (i + 1)). * exact (to_Pr1 (to_BinDirectSums A (C1 (i + 1)) (C2 i))). * use compose. -- exact (C2' i). -- exact (transportf (precategory_morphisms (C1 (i + 1))) (maponpaths C2' (hzrplusminus i 1)) (H (i + 1))). -- exact (to_In2 (to_BinDirectSums A (C1' (i + 1)) (C2' i))). + use compose. * exact (C2 i). * exact (to_Pr2 (to_BinDirectSums A (C1 (i + 1)) (C2 i))). * use compose. -- exact (C2' i). -- exact (g2 i). -- exact (to_In2 (to_BinDirectSums A (C1' (i + 1)) (C2' i))). 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.