∀ {C : Type u_5} [inst : CategoryTheory.Category.{u_3, u_5} C] {D : Type u_6}
  [inst_1 : CategoryTheory.Category.{u_4, u_6} D] {J : Type u_2} [inst_2 : CategoryTheory.Category.{u_1, u_2} J]
  {K : CategoryTheory.Functor J C} {F G : CategoryTheory.Functor C D} (h : F ≅ G) [CategoryTheory.CreatesLimit K F],
  CategoryTheory.Limits.ReflectsLimit K G