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 16714
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 16712 . 2 class Yon
2 vc . . 3 setvar 𝑐
3 ccat 16148 . . 3 class Cat
42cv 1474 . . . . 5 class 𝑐
5 coppc 16194 . . . . . 6 class oppCat
64, 5cfv 5804 . . . . 5 class (oppCat‘𝑐)
74, 6cop 4131 . . . 4 class 𝑐, (oppCat‘𝑐)⟩
8 chof 16711 . . . . 5 class HomF
96, 8cfv 5804 . . . 4 class (HomF‘(oppCat‘𝑐))
10 ccurf 16673 . . . 4 class curryF
117, 9, 10co 6549 . . 3 class (⟨𝑐, (oppCat‘𝑐)⟩ curryF (HomF‘(oppCat‘𝑐)))
122, 3, 11cmpt 4643 . 2 class (𝑐 ∈ Cat ↦ (⟨𝑐, (oppCat‘𝑐)⟩ curryF (HomF‘(oppCat‘𝑐))))
131, 12wceq 1475 1 wff Yon = (𝑐 ∈ Cat ↦ (⟨𝑐, (oppCat‘𝑐)⟩ curryF (HomF‘(oppCat‘𝑐))))
Colors of variables: wff setvar class
This definition is referenced by:  yonval  16724
  Copyright terms: Public domain W3C validator