{J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    {F : CategoryTheory.Functor J (Type w₀)} →
      (pt : Type w₁) →
        (ι : (j : J) → F.obj j → pt) →
          autoParam (∀ {j j' : J} (f : j ⟶ j'), ι j' ∘ F.map f = ι j)
              CategoryTheory.Functor.CoconeTypes.ι_naturality._autoParam →
            F.CoconeTypes