English
The uncurrying functor converts a functor C ⥤ D ⥤ E into a functor C × D ⥤ E by sending (X,Y) ↦ F.obj (X,Y) with appropriate maps.
Русский
Функтор раскрещивания переводит функтор C ⥤ D ⥤ E в функтор C × D ⥤ E: (X,Y) ↦ F.obj (X,Y) со структурными отображениями.
LaTeX
$$$ \mathrm{uncurry} : (C \;\to\; D \;\to\; E) \to (C \times D \to E). $$$
Lean4
/-- The currying functor, taking a functor `(C × D) ⥤ E` and producing a functor `C ⥤ (D ⥤ E)`.
-/
@[simps! obj_obj_obj obj_obj_map obj_map_app map_app_app]
def curry : (C × D ⥤ E) ⥤ C ⥤ D ⥤ E where
obj F := curryObj F
map
T :=
{ app := fun X =>
{ app := fun Y => T.app (X, Y)
naturality := fun Y Y' g => by
dsimp [curryObj]
rw [NatTrans.naturality] }
naturality := fun X X' f => by
ext; dsimp [curryObj]
rw [NatTrans.naturality] }
-- create projection simp lemmas even though this isn't a `{ .. }`.
