Combining functors

Stream: Is there code for X?

[Adam Topaz]

Does the following construction have a name? Is there a straightforward way to define this with what we have in mathlib?

import category_theory.limits.shapes.binary_products

open category_theory
variables (J C : Type*) [category J] [category C]
  (F G : J ⥤ C) (M : C ⥤ C ⥤ C)

example : J ⥤ C :=
{ obj := λ j, (M.obj $ F.obj j).obj $ G.obj j,
  map := λ i j f, (M.map (F.map f)).app (G.obj i) ≫ (M.obj (F.obj j)).map (G.map f) }

[Adam Topaz]

I guess one way to construct this is to use the diagonal functor J ⥤ J × J, compose that with F.prod G, and the uncurried version of M.

[Adam Topaz]

But I can't seem to find the functor J ⥤ J × J in mathlib.

[Adam Topaz]

import category_theory.limits.shapes.binary_products
import category_theory.currying

open category_theory
variables (J C : Type*) [category J] [category C]
  (F G : J ⥤ C) (M : C ⥤ C ⥤ C)

def foo : J ⥤ C :=
{ obj := λ j, (M.obj $ F.obj j).obj $ G.obj j,
  map := λ i j f, (M.map (F.map f)).app (G.obj i) ≫ (M.obj (F.obj j)).map (G.map f) }

def bar : J ⥤ C :=
{ obj := λ j, (j,j),
  map := λ _ _ f, (f,f) } ⋙ F.prod G ⋙ (uncurry.obj M)

example : foo = bar := rfl