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 17099
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 17097 . 2 class Yon
2 vc . . 3 setvar 𝑐
3 ccat 16532 . . 3 class Cat
42cv 1630 . . . . 5 class 𝑐
5 coppc 16578 . . . . . 6 class oppCat
64, 5cfv 6031 . . . . 5 class (oppCat‘𝑐)
74, 6cop 4322 . . . 4 class 𝑐, (oppCat‘𝑐)⟩
8 chof 17096 . . . . 5 class HomF
96, 8cfv 6031 . . . 4 class (HomF‘(oppCat‘𝑐))
10 ccurf 17058 . . . 4 class curryF
117, 9, 10co 6793 . . 3 class (⟨𝑐, (oppCat‘𝑐)⟩ curryF (HomF‘(oppCat‘𝑐)))
122, 3, 11cmpt 4863 . 2 class (𝑐 ∈ Cat ↦ (⟨𝑐, (oppCat‘𝑐)⟩ curryF (HomF‘(oppCat‘𝑐))))
131, 12wceq 1631 1 wff Yon = (𝑐 ∈ Cat ↦ (⟨𝑐, (oppCat‘𝑐)⟩ curryF (HomF‘(oppCat‘𝑐))))
Colors of variables: wff setvar class
This definition is referenced by:  yonval  17109
  Copyright terms: Public domain W3C validator