∀ (C : Type u_2) [inst : CategoryTheory.Category.{u_3, u_2} C] (A : Type u_5)
  [inst_1 : CategoryTheory.Category.{u_4, u_5} A] [inst_2 : CategoryTheory.Limits.HasCoproducts A]
  {X Y : CategoryTheory.Functor C A} (α : X ⟶ Y) ⦃X_1 Y_1 : CategoryTheory.Limits.FormalCoproduct C⦄ (f : X_1 ⟶ Y_1),
  CategoryTheory.CategoryStruct.comp
      ({ obj := fun X_2 => ∐ fun i => X.obj (X_2.obj i),
            map := fun {X_2 Y} f =>
              CategoryTheory.Limits.Sigma.desc fun i =>
                CategoryTheory.CategoryStruct.comp (X.map (f.φ i))
                  (CategoryTheory.Limits.Sigma.ι (X.obj ∘ Y.obj) (f.f i)),
            map_id := ⋯, map_comp := ⋯ }.map
        f)
      (CategoryTheory.Limits.Sigma.map fun i => α.app (Y_1.obj i)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.map fun i => α.app (X_1.obj i))
      ({ obj := fun X => ∐ fun i => Y.obj (X.obj i),
            map := fun {X Y_2} f =>
              CategoryTheory.Limits.Sigma.desc fun i =>
                CategoryTheory.CategoryStruct.comp (Y.map (f.φ i))
                  (CategoryTheory.Limits.Sigma.ι (Y.obj ∘ Y_2.obj) (f.f i)),
            map_id := ⋯, map_comp := ⋯ }.map
        f)