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

Definition df-yon 16885
 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 16883 . 2 class Yon
2 vc . . 3 setvar 𝑐
3 ccat 16319 . . 3 class Cat
42cv 1481 . . . . 5 class 𝑐
5 coppc 16365 . . . . . 6 class oppCat
64, 5cfv 5886 . . . . 5 class (oppCat‘𝑐)
74, 6cop 4181 . . . 4 class 𝑐, (oppCat‘𝑐)⟩
8 chof 16882 . . . . 5 class HomF
96, 8cfv 5886 . . . 4 class (HomF‘(oppCat‘𝑐))
10 ccurf 16844 . . . 4 class curryF
117, 9, 10co 6647 . . 3 class (⟨𝑐, (oppCat‘𝑐)⟩ curryF (HomF‘(oppCat‘𝑐)))
122, 3, 11cmpt 4727 . 2 class (𝑐 ∈ Cat ↦ (⟨𝑐, (oppCat‘𝑐)⟩ curryF (HomF‘(oppCat‘𝑐))))
131, 12wceq 1482 1 wff Yon = (𝑐 ∈ Cat ↦ (⟨𝑐, (oppCat‘𝑐)⟩ curryF (HomF‘(oppCat‘𝑐))))
 Colors of variables: wff setvar class This definition is referenced by:  yonval  16895
 Copyright terms: Public domain W3C validator