∀ (C : Type u_3) [inst : CategoryTheory.Category.{u_2, u_3} C] (α : Type u_1)
  [inst_1 : CategoryTheory.Limits.HasFiniteCoproducts C] {X Y Z : CategoryTheory.Functor (CategoryTheory.Discrete α) C}
  (f : X ⟶ Y) (g : Y ⟶ Z),
  { app := fun x => CategoryTheory.Limits.Sigma.map fun x_1 => (CategoryTheory.CategoryStruct.comp f g).app ↑x_1,
      naturality := ⋯ } =
    CategoryTheory.CategoryStruct.comp
      { app := fun x => CategoryTheory.Limits.Sigma.map fun x_1 => f.app ↑x_1, naturality := ⋯ }
      { app := fun x => CategoryTheory.Limits.Sigma.map fun x_1 => g.app ↑x_1, naturality := ⋯ }