{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : LinearOrder J] →
        [inst_2 : OrderBot J] →
          {F : CategoryTheory.Functor J C} →
            (c : CategoryTheory.Limits.Cocone F) → {X Y : C} → (X ⟶ Y) → (F.obj ⊥ ⟶ X) → (c.pt ⟶ Y) → J → Type v