∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_4, u_3} C] (D : Type u_2)
  [inst_1 : CategoryTheory.Category.{u_1, u_2} D]
  [inst_2 : ∀ (a b : C), CategoryTheory.Limits.HasCoproductsOfShape (a ⟶ b) D] (c : C) {X Y Z : D} (f : X ⟶ Y)
  (g : Y ⟶ Z),
  {
      app := fun x =>
        CategoryTheory.Limits.Sigma.desc fun h =>
          CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g)
            (CategoryTheory.Limits.Sigma.ι (fun x => Z) h),
      naturality := ⋯ } =
    CategoryTheory.CategoryStruct.comp
      {
        app := fun x =>
          CategoryTheory.Limits.Sigma.desc fun h =>
            CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.Sigma.ι (fun x => Y) h),
        naturality := ⋯ }
      {
        app := fun x =>
          CategoryTheory.Limits.Sigma.desc fun h =>
            CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.Sigma.ι (fun x => Z) h),
        naturality := ⋯ }