∀ {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 : CategoryTheory.Functor Cᵒᵖ D)
  [CategoryTheory.CreatesColimit K.leftOp F.rightOp], CategoryTheory.Limits.ReflectsLimit K F