English
The Yoneda pairing is the functor that sends a pair (X^op, F) to the set (Yoneda op X) ⟶ F, i.e., to the morphisms from yoneda.op.obj X to F, functorially in both X and F.
Русский
Паринг Ёнеда — функтор, который отправляет пару (X^op, F) в множество (yoneda.op.obj X) ⟶ F, т.е. морфизмы из yoneda.op.obj X в F, функционально по обоим аргументам.
LaTeX
$$$\text{yonedaPairing} : C^{op} \times (C^{op} ⥤ Type) \to Type$ with $(X,F) \mapsto \yoneda.op.obj X \to F$$$
Lean4
/-- The "Yoneda pairing" functor, which sends `X : Cᵒᵖ` and `F : Cᵒᵖ ⥤ Type`
to `yoneda.op.obj X ⟶ F`, functorially in both `X` and `F`.
-/
def yonedaPairing : Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁) ⥤ Type max u₁ v₁ :=
Functor.prod yoneda.op (𝟭 (Cᵒᵖ ⥤ Type v₁)) ⋙ Functor.hom (Cᵒᵖ ⥤ Type v₁)
