Definition df-yon 18296

Description: Define the Yoneda embedding, which is the currying of the (opposite) Hom functor. (Contributed by Mario Carneiro, 11-Jan-2017.)

Assertion

Ref	Expression
df-yon	⊢ Yon = (𝑐 ∈ Cat ↦ (⟨𝑐, (oppCat‘𝑐)⟩ curryF (HomF‘(oppCat‘𝑐))))

Detailed syntax breakdown of Definition df-yon

Step	Hyp	Ref	Expression
1		cyon 18294	. 2 class Yon
2		vc	. . 3 setvar 𝑐
3		ccat 17707	. . 3 class Cat
4	2	cv 1539	. . . . 5 class 𝑐
5		coppc 17754	. . . . . 6 class oppCat
6	4, 5	cfv 6561	. . . . 5 class (oppCat‘𝑐)
7	4, 6	cop 4632	. . . 4 class ⟨𝑐, (oppCat‘𝑐)⟩
8		chof 18293	. . . . 5 class HomF
9	6, 8	cfv 6561	. . . 4 class (HomF‘(oppCat‘𝑐))
10		ccurf 18255	. . . 4 class curryF
11	7, 9, 10	co 7431	. . 3 class (⟨𝑐, (oppCat‘𝑐)⟩ curryF (HomF‘(oppCat‘𝑐)))
12	2, 3, 11	cmpt 5225	. 2 class (𝑐 ∈ Cat ↦ (⟨𝑐, (oppCat‘𝑐)⟩ curryF (HomF‘(oppCat‘𝑐))))
13	1, 12	wceq 1540	1 wff Yon = (𝑐 ∈ Cat ↦ (⟨𝑐, (oppCat‘𝑐)⟩ curryF (HomF‘(oppCat‘𝑐))))

This definition is referenced by:  yonval  18306