English
The Coyoneda pairing is the bifunctor that sends a pair (X, F) with X ∈ C and F ∈ C ⥤ Type to the set of morphisms coyoneda.obj X ⟶ F in the functor category. It is functorial in both X and F.
Русский
СоединениеCoyoneda — бифунктор, который сопоставляет паре (X, F) с X ∈ C и F ∈ C ⥤ Type множество морфизмов coyoneda.obj X ⟶ F в категории функторов; он функториален по обоим аргументам.
LaTeX
$$$$ (coyonedaPairing(C))(X,F) = \mathrm{Hom}(coyoneda.obj(X),F) $$$$
Lean4
/-- The "Coyoneda pairing" functor, which sends `X : C` and `F : C ⥤ Type`
to `coyoneda.rightOp.obj X ⟶ F`, functorially in both `X` and `F`.
-/
def coyonedaPairing : C × (C ⥤ Type v₁) ⥤ Type max u₁ v₁ :=
Functor.prod coyoneda.rightOp (𝟭 (C ⥤ Type v₁)) ⋙ Functor.hom (C ⥤ Type v₁)
