Metamath Proof Explorer

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 = ( c e. Cat |-> ( <. c , ( oppCat ` c ) >. curryF ( HomF ` ( oppCat ` c ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cyon 
 |-  Yon
1 vc 
 |-  c
2 ccat 
 |-  Cat
3 1 cv 
 |-  c
4 coppc 
 |-  oppCat
5 3 4 cfv 
 |-  ( oppCat ` c )
6 3 5 cop 
 |-  <. c , ( oppCat ` c ) >.
7 ccurf 
 |-  curryF
8 chof 
 |-  HomF
9 5 8 cfv 
 |-  ( HomF ` ( oppCat ` c ) )
10 6 9 7 co 
 |-  ( <. c , ( oppCat ` c ) >. curryF ( HomF ` ( oppCat ` c ) ) )
11 1 2 10 cmpt 
 |-  ( c e. Cat |-> ( <. c , ( oppCat ` c ) >. curryF ( HomF ` ( oppCat ` c ) ) ) )
12 0 11 wceq 
 |-  Yon = ( c e. Cat |-> ( <. c , ( oppCat ` c ) >. curryF ( HomF ` ( oppCat ` c ) ) ) )