Definition df-yon

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cyon	⊢ Yon
1		vc	⊢ 𝑐
2		ccat	⊢ Cat
3	1	cv	⊢ 𝑐
4		coppc	⊢ oppCat
5	3 4	cfv	⊢ ( oppCat ‘ 𝑐 )
6	3 5	cop	⊢ ⟨ 𝑐 , ( oppCat ‘ 𝑐 ) ⟩
7		ccurf	⊢ curryF
8		chof	⊢ HomF
9	5 8	cfv	⊢ ( HomF ‘ ( oppCat ‘ 𝑐 ) )
10	6 9 7	co	⊢ ( ⟨ 𝑐 , ( oppCat ‘ 𝑐 ) ⟩ curryF ( HomF ‘ ( oppCat ‘ 𝑐 ) ) )
11	1 2 10	cmpt	⊢ ( 𝑐 ∈ Cat ↦ ( ⟨ 𝑐 , ( oppCat ‘ 𝑐 ) ⟩ curryF ( HomF ‘ ( oppCat ‘ 𝑐 ) ) ) )
12	0 11	wceq	⊢ Yon = ( 𝑐 ∈ Cat ↦ ( ⟨ 𝑐 , ( oppCat ‘ 𝑐 ) ⟩ curryF ( HomF ‘ ( oppCat ‘ 𝑐 ) ) ) )