MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-yon Unicode version

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

Detailed syntax breakdown of Definition df-yon
StepHypRef Expression
1 cyon 14023 . 2  class Yon
2 vc . . 3  set  c
3 ccat 13566 . . 3  class  Cat
42cv 1622 . . . . 5  class  c
5 coppc 13614 . . . . . 6  class oppCat
64, 5cfv 5255 . . . . 5  class  (oppCat `  c )
74, 6cop 3643 . . . 4  class  <. c ,  (oppCat `  c ) >.
8 chof 14022 . . . . 5  class HomF
96, 8cfv 5255 . . . 4  class  (HomF `  (oppCat `  c ) )
10 ccurf 13984 . . . 4  class curryF
117, 9, 10co 5858 . . 3  class  ( <.
c ,  (oppCat `  c ) >. curryF  (HomF
`  (oppCat `  c )
) )
122, 3, 11cmpt 4077 . 2  class  ( c  e.  Cat  |->  ( <.
c ,  (oppCat `  c ) >. curryF  (HomF
`  (oppCat `  c )
) ) )
131, 12wceq 1623 1  wff Yon  =  ( c  e.  Cat  |->  (
<. c ,  (oppCat `  c ) >. curryF  (HomF
`  (oppCat `  c )
) ) )
Colors of variables: wff set class
This definition is referenced by:  yonval  14035
  Copyright terms: Public domain W3C validator