English
The currying functor establishes an equivalence of categories between C ⥤ D ⥤ E and (C × D) ⥤ E, with inverse given by uncurry.
Русский
Функтор каррирования устанавливает эквивалентность категорий между C ⥤ D ⥤ E и (C × D) ⥤ E, обратный каррированию — раскрещивание.
LaTeX
$$$ \mathrm{curry} : (C \times D \to E) \cong (C \to D \to E) \quad \text{and} \quad \mathrm{uncurry} : (C \to D \to E) \to (C \times D \to E). $$$
Lean4
/-- The object level part of the currying functor. (See `curry` for the functorial version.)
-/
def curryObj (F : C × D ⥤ E) : C ⥤ D ⥤ E
where
obj
X :=
{ obj := fun Y => F.obj (X, Y)
map := fun g => F.map (𝟙 X, g)
map_id := fun Y => by simp only; rw [← prod_id]; exact F.map_id ⟨X, Y⟩
map_comp := fun f g => by simp [← F.map_comp] }
map
f :=
{ app := fun Y => F.map (f, 𝟙 Y)
naturality := fun {Y} {Y'} g => by simp [← F.map_comp] }
map_id := fun X => by ext Y; exact F.map_id _
map_comp := fun f g => by ext Y; simp [← F.map_comp]
