Concrete description of (co)limits in functor categories

Some of the concrete descriptions of (co)limits in Type v extend to (co)limits in the functor category K ⥤ Type v.

theorem CategoryTheory.FunctorToTypes.jointly_surjective {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] (F : CategoryTheory.Functor J (CategoryTheory.Functor K TypeMax)) (k : K) {t : CategoryTheory.Limits.Cocone F} (h : CategoryTheory.Limits.IsColimit t) (x : t.pt.obj k) : ∃ (j : J) (y : (F.obj j).obj k), x = (t.ι.app j).app k y

theorem CategoryTheory.FunctorToTypes.jointly_surjective' {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] (F : CategoryTheory.Functor J (CategoryTheory.Functor K TypeMax)) (k : K) (x : (CategoryTheory.Limits.colimit F).obj k) : ∃ (j : J) (y : (F.obj j).obj k), x = (CategoryTheory.Limits.colimit.ι F j).app k y