{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {J : Type u} →
      [inst_1 : LinearOrder J] →
        {j : J} →
          {F : CategoryTheory.Functor (↑(Set.Iio j)) C} →
            (c : CategoryTheory.Limits.Cocone F) →
              (i : J) → (hi : i < j) → (CategoryTheory.SmallObject.SuccStruct.ofCocone c).obj ⟨i, ⋯⟩ ≅ F.obj ⟨i, hi⟩