∀ {α : Type u} {J : Type w} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.FinCategory J]
  [inst_2 : SemilatticeSup α] [inst_3 : OrderBot α] (F : CategoryTheory.Functor J α),
  CategoryTheory.Limits.colimit F = Finset.univ.sup F.obj