English
For categories C and D, there is a canonical functor evaluationUncurried: C × (C ⥤ D) ⥤ D defined by sending a pair (X, F) to F(X). On morphisms it acts by composing the action of F on morphisms with the component of the natural transformation on the target object.
Русский
Для категорий C и D существует канонический функтор evaluationUncurried: C × (C ⥤ D) ⥤ D, который отправляет пару (X, F) в F(X). На морфизмах действует путем композиции отображения F на морфизм и компоненты натурального преобразования в целевом объекте.
LaTeX
$$$\\mathrm{evaluationUncurried}: C \\times (C \\to D) \\to D$ is defined by $(X,F) \\mapsto F(X)$ and, on morphisms, by the natural action induced by the functor $F$ and the morphism part of the second component.$$
Lean4
/-- The "evaluation of `F` at `X`" functor,
as a functor `C × (C ⥤ D) ⥤ D`.
-/
@[simps]
def evaluationUncurried : C × (C ⥤ D) ⥤ D where
obj p := p.2.obj p.1
map := fun {x} {y} f => x.2.map f.1 ≫ f.2.app y.1
