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

Definition df-yon 15053
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 15051 . 2  class Yon
2 vc . . 3  setvar  c
3 ccat 14594 . . 3  class  Cat
42cv 1368 . . . . 5  class  c
5 coppc 14642 . . . . . 6  class oppCat
64, 5cfv 5413 . . . . 5  class  (oppCat `  c )
74, 6cop 3878 . . . 4  class  <. c ,  (oppCat `  c ) >.
8 chof 15050 . . . . 5  class HomF
96, 8cfv 5413 . . . 4  class  (HomF `  (oppCat `  c ) )
10 ccurf 15012 . . . 4  class curryF
117, 9, 10co 6086 . . 3  class  ( <.
c ,  (oppCat `  c ) >. curryF  (HomF
`  (oppCat `  c )
) )
122, 3, 11cmpt 4345 . 2  class  ( c  e.  Cat  |->  ( <.
c ,  (oppCat `  c ) >. curryF  (HomF
`  (oppCat `  c )
) ) )
131, 12wceq 1369 1  wff Yon  =  ( c  e.  Cat  |->  (
<. c ,  (oppCat `  c ) >. curryF  (HomF
`  (oppCat `  c )
) ) )
Colors of variables: wff setvar class
This definition is referenced by:  yonval  15063
  Copyright terms: Public domain W3C validator