∀ {J : Type u_4} {C : Type u_2} [inst : CategoryTheory.Category.{u_3, u_4} J]
  [inst_1 : CategoryTheory.Category.{u_1, u_2} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  (F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C))
  [inst_3 : CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₁)]
  [inst_4 : CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₂)]
  [inst_5 : CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₃)] (x x_1 : J) (f : x ⟶ x_1),
  CategoryTheory.CategoryStruct.comp (F.map f)
      { τ₁ := CategoryTheory.Limits.colimit.ι (F.comp CategoryTheory.ShortComplex.π₁) x_1,
        τ₂ := CategoryTheory.Limits.colimit.ι (F.comp CategoryTheory.ShortComplex.π₂) x_1,
        τ₃ := CategoryTheory.Limits.colimit.ι (F.comp CategoryTheory.ShortComplex.π₃) x_1, comm₁₂ := ⋯, comm₂₃ := ⋯ } =
    CategoryTheory.CategoryStruct.comp
      { τ₁ := CategoryTheory.Limits.colimit.ι (F.comp CategoryTheory.ShortComplex.π₁) x,
        τ₂ := CategoryTheory.Limits.colimit.ι (F.comp CategoryTheory.ShortComplex.π₂) x,
        τ₃ := CategoryTheory.Limits.colimit.ι (F.comp CategoryTheory.ShortComplex.π₃) x, comm₁₂ := ⋯, comm₂₃ := ⋯ }
      (((CategoryTheory.Functor.const J).obj
            { X₁ := CategoryTheory.Limits.colimit (F.comp CategoryTheory.ShortComplex.π₁),
              X₂ := CategoryTheory.Limits.colimit (F.comp CategoryTheory.ShortComplex.π₂),
              X₃ := CategoryTheory.Limits.colimit (F.comp CategoryTheory.ShortComplex.π₃),
              f := CategoryTheory.Limits.colimMap (F.whiskerLeft CategoryTheory.ShortComplex.π₁Toπ₂),
              g := CategoryTheory.Limits.colimMap (F.whiskerLeft CategoryTheory.ShortComplex.π₂Toπ₃), zero := ⋯ }).map
        f)