∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {F : CategoryTheory.Functor J (Type w₀)} (c : F.CoconeTypes)
  {J' : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} J'] (G : CategoryTheory.Functor J' J),
  (c.precomp G).pt = c.pt