English
The Yoneda evaluation is the evaluation functor that sends a pair (X^op, F) to F.obj X, i.e., it evaluates F at X. It is functorial in both arguments.
Русский
Оценка Ёнеда — это функтор оценки, отправляющий пару (X^op, F) в F.obj X; то есть он производит значение F на X. Функторность сохраняется по обоим аргументам.
LaTeX
$$$\mathrm{yonedaEvaluation}\; C: C^{op} \times (C^{op} \Hookrightarrow Type) \to Type\;\text{ satisfies}\; (\mathrm{yonedaEvaluation}\; C).obj (X, F) = F.obj X$$$
Lean4
/-- The "Yoneda evaluation" functor, which sends `X : Cᵒᵖ` and `F : Cᵒᵖ ⥤ Type`
to `F.obj X`, functorially in both `X` and `F`.
-/
def yonedaEvaluation : Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁) ⥤ Type max u₁ v₁ :=
evaluationUncurried Cᵒᵖ (Type v₁) ⋙ uliftFunctor
