# The Yoneda Lemma

Representable Functor F of C ( a, -):

$\boxed {(-)^{a} = \text {F} \iff a = \text {log F}}$

Video 4.2 Yoneda Lemma

Prove :

Yoneda Lemma :
$\text {F :: C} \to \text {Set}$

$\boxed {\alpha \text { :: [C, Set] (C (a, -),F) } \simeq \text {F a}}$

$\alpha : \text {Natural Transformation}$
$\simeq : \text {(Natural) Isomorphism, "naturally" } \forall ( a, F )$

Proof: By “Diagram chasing” below, shows that

Left-side
: $\alpha \text { :: [C, Set] (C (a, -),F) }$ is indeed a (co-variant) Functor. (Higher-order Function)

Right-side: Functor “F a“. (Data Structure)

$\boxed {\forall x, (a \to x) \to \text { F } x \simeq \text { F } a }$

Note: When talking about the natural transformations, always mention their component “x”: $\alpha_{x}, \beta_{x}$

Video 5.1 Yoneda Embedding

Example 1: F = List functor [x]

$\boxed {\alpha \text { :: } (a \to x) \to [x] \simeq [a] }$

Example 2: F = C (b, -)

$\boxed {\alpha \text { :: [C, Set] (C (a, -), C (b, -) ) } \simeq \text {C (b, a)}}$

Note: check a , b is in co-variant or contra-variant position.

Example 3: F = Id

$\boxed {\alpha \text { :: } (a \to x) \to x \simeq a }$

Right-hand-side: a (data structure)

Left-hand-side : “(a -> x) “is a function called “handler” (or “continuation“) which takes the argument “a” to provide it as output : “(a -> x ) -> x“.

eg. handler to database query, over internet…(technique used in Compiler)

Co-Yoneda Lemma : (Contra-variant a , F)

$\boxed {\alpha \text { :: [C, Set] (C(-, a),F) } \simeq \text {F a}}$

Yoneda Embedding: Full and Faithful
$\alpha \text { :: [C, Set] (C (a, -), C (b, -) ) } \simeq \text {C (b, a)}$

Note: Instead of proving a , b are isomorphic, sometimes it is easier to prove the functors C(a, -) & C(b, -) are isomorphic.[Proof Trivial: functors preserve composition and identity]

ApplicationCo-Yoneda Lemma : (Contra-variant a , F)
$\boxed {\text {[C, Set] (C(- , a), C(- , b) } \simeq \text {C(a ,b)}}$

Pre-order Category $\boxed {a \leq b}$

$\forall x, \text {C(x , a)} \to \text {C(x , b)} \simeq \text {C(a , b)}$

$C(x , a) = x \leq a = \{\varnothing, 1 \}$
$C(x , b) = x \leq b =\{\varnothing, 1 \}$

3 possibilities: (“1” = singleton)
$id_{\varnothing} :: \varnothing \to \varnothing$
$absurd :: \varnothing \to 1$
$id_{1} :: 1 \to 1$
Note: $1 \to \varnothing$ impossible (function must have an image)

Verify

Right-Hand Side: $a \leq b$

Left-Hand Side: $\forall x,( x \leq a \implies x \leq b) \implies a \leq b$

Yoneda Embedding (Lagatta)