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

Definition df-yon 18145
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
StepHypRef Expression
1 cyon 18143 . 2 class Yon
2 vc . . 3 setvar ๐‘
3 ccat 17549 . . 3 class Cat
42cv 1541 . . . . 5 class ๐‘
5 coppc 17596 . . . . . 6 class oppCat
64, 5cfv 6497 . . . . 5 class (oppCatโ€˜๐‘)
74, 6cop 4593 . . . 4 class โŸจ๐‘, (oppCatโ€˜๐‘)โŸฉ
8 chof 18142 . . . . 5 class HomF
96, 8cfv 6497 . . . 4 class (HomFโ€˜(oppCatโ€˜๐‘))
10 ccurf 18104 . . . 4 class curryF
117, 9, 10co 7358 . . 3 class (โŸจ๐‘, (oppCatโ€˜๐‘)โŸฉ curryF (HomFโ€˜(oppCatโ€˜๐‘)))
122, 3, 11cmpt 5189 . 2 class (๐‘ โˆˆ Cat โ†ฆ (โŸจ๐‘, (oppCatโ€˜๐‘)โŸฉ curryF (HomFโ€˜(oppCatโ€˜๐‘))))
131, 12wceq 1542 1 wff Yon = (๐‘ โˆˆ Cat โ†ฆ (โŸจ๐‘, (oppCatโ€˜๐‘)โŸฉ curryF (HomFโ€˜(oppCatโ€˜๐‘))))
Colors of variables: wff setvar class
This definition is referenced by:  yonval  18155
  Copyright terms: Public domain W3C validator