∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} C] [CategoryTheory.GaloisCategory C]
  (F : CategoryTheory.Functor C FintypeCat) (X : C),
  CategoryTheory.Limits.HasLimit (CategoryTheory.Discrete.functor fun x => X)