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 (Type w))) (k : K) {t : CategoryTheory.Limits.Cocone F} (h : CategoryTheory.Limits.IsColimit t) (x : t.pt.obj k) [∀ (k : K), CategoryTheory.Limits.HasColimit (F.flip.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 (Type w))) [∀ (k : K), CategoryTheory.Limits.HasColimit (F.flip.obj k)] (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

theorem CategoryTheory.FunctorToTypes.colimit.map_ι_apply {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] (F : CategoryTheory.Functor J (CategoryTheory.Functor K (Type w))) [CategoryTheory.Limits.HasColimit F] (j : J) {k k' : K} {f : k ⟶ k'} {x : (F.obj j).obj k} : (CategoryTheory.Limits.colimit F).map f ((CategoryTheory.Limits.colimit.ι F j).app k x) = (CategoryTheory.Limits.colimit.ι F j).app k' ((F.obj j).map f x)