Metamath Proof Explorer

Definition df-yon

Description: Define the Yoneda embedding, which is the currying of the (opposite) Hom functor. (Contributed by Mario Carneiro, 11-Jan-2017)

Ref Expression
Assertion df-yon ⊢ Yon = c ∈ Cat ⟼ c oppCat ⁡ c curry F Hom F ⁡ oppCat ⁡ c

Detailed syntax breakdown

Step Hyp Ref Expression
0 cyon class Yon
1 vc setvar c
2 ccat class Cat
3 1 cv setvar c
4 coppc class oppCat
5 3 4 cfv class oppCat ⁡ c
6 3 5 cop class c oppCat ⁡ c
7 ccurf class curry F
8 chof class Hom F
9 5 8 cfv class Hom F ⁡ oppCat ⁡ c
10 6 9 7 co class c oppCat ⁡ c curry F Hom F ⁡ oppCat ⁡ c
11 1 2 10 cmpt class c ∈ Cat ⟼ c oppCat ⁡ c curry F Hom F ⁡ oppCat ⁡ c
12 0 11 wceq wff Yon = c ∈ Cat ⟼ c oppCat ⁡ c curry F Hom F ⁡ oppCat ⁡ c