∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u))
  (c : CategoryTheory.Limits.Cocone F) (j : J) (a : F.obj j), (F.coconeTypesEquiv.symm c).ι j a = c.ι.app j a