English
The Coyoneda evaluation is the functor that sends a pair (X, F) with X an object of C and F a functor C ⥤ Type to the value F(X). It is functorial in both X and F, i.e., it is the evaluation functor on the product category, possibly adjusted for universe levels.
Русский
ОценкаCoyonеда — это функтор, отображающий пару (X, F) с X — объект C и F — функтор C ⥤ Type в значение F(X); он допустимо коррелируется по обоим параметрам X и F, то есть это обычная оценочная функция из произведения категорий.
LaTeX
$$$$ \mathrm{coyonedaEvaluation}(X,F) = F(X) \,.$$$$
Lean4
/-- The "Coyoneda evaluation" functor, which sends `X : C` and `F : C ⥤ Type`
to `F.obj X`, functorially in both `X` and `F`.
-/
def coyonedaEvaluation : C × (C ⥤ Type v₁) ⥤ Type max u₁ v₁ :=
evaluationUncurried C (Type v₁) ⋙ uliftFunctor
