∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} C] {α : Type u_1}
  [inst_1 : CategoryTheory.Limits.HasFiniteCoproducts C] (F : CategoryTheory.Functor (CategoryTheory.Discrete α) C)
  {X Y Z : Finset (CategoryTheory.Discrete α)} (f : X ⟶ Y) (g : Y ⟶ Z),
  (CategoryTheory.Limits.Sigma.desc fun y => CategoryTheory.Limits.Sigma.ι (fun x => F.obj ↑x) ⟨↑y, ⋯⟩) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.Sigma.desc fun y => CategoryTheory.Limits.Sigma.ι (fun x => F.obj ↑x) ⟨↑y, ⋯⟩)
      (CategoryTheory.Limits.Sigma.desc fun y => CategoryTheory.Limits.Sigma.ι (fun x => F.obj ↑x) ⟨↑y, ⋯⟩)