type Hom a b = (a -> b)type Nat f g = forall x. f x -> g x

Yoneda, which states that $[C, Set](F(-), Hom(a, -)) \simeq F(a)$:

type YonedaLHS f a = Nat (Hom a) f

rhs2lhs :: Functor g => g a -> YonedaLHS g a-- rhs2lhs :: g a -> (Nat (Hom a) g)-- rhs2lhs :: g a -> (forall x. (Hom a) x ->  g x)-- rhs2lhs :: g a -> (forall x. (a -> x) -> g x)rhs2lhs ga = (\a2x -> fmap a2x ga) :: g x

rhs2lhs is a lot like an enriched continuation, where we are given a value (g a), and we need to produce an "enriched" continuation handler, which when given a use (a -> x) produces not an x, but a g x.

lhs2rhs :: Functor g => YonedaLHS g a -> g a-- lhs2rhs :: Nat (Hom a) g -> g a-- lhs2rhs :: (forall x. (Hom a x) -> g x) -> g a-- lhs2rhs :: (forall x. (a -> x) -> g x) -> g a-- set x = a-- lhs2rhs :: ((a -> a) -> g a) -> g alhs2rhs cont = (cont (id :: Hom a a)) :: g a

in lhs2rhs, given an enriched continuation handler forall x. (a -> x) -> g x, and we need to produce a g a. As with regular continuations, we feed in the id function to recover the trapped continuation value.

type List a = [a]type Nat f g = forall x. f x -> g xlistyo :: (Nat (Hom a) List) -> [a]-- listyo :: (forall x. (Hom a x) -> List x) -> [a]-- listyo :: (f: forall x. (g: a -> x) -> [x]) -> [a]-- implement f, is to use g multiple times-- f g = [g a1, g a2, ... g an] = fmap g [a1, a2, ... an]-- f id = [id a1, id a2, ... id an] = [a1, a2, ... an]listyo f = f id-- F = [.]listyo' ::  [a] -> (forall x. (a-> x) -> [x])listyo' as = \f -> fmap f as

When we specialize Yoneda to lists, we are led to the idea that a continuation of the form (a -> x) -> [x] must contain [a]s which it uses to produce multiple xs.

-- F = (b -> .)-- pick x = a-- ((a -> a) -> (b -> a) -> (b -> a)-- Nat(Hom(a, -), F) ~= F a-- type Hom a b = (a -> b)-- c -> Hom (c, -)-- a, b. arrows ∈ Hom (a, b)-- Hom (a, -), Hom(b, -). arrows ∈ Nat Hom (a, -) Hom(b, -)---- a, b. arrows ∈ Hom (a, b)-- Hom (-, a), Hom(-, b). arrows ∈ Nat Hom (-, a) Hom(-, b)contrayo :: Nat (Hom a) (Hom b) -> Hom b acontrayo :: (forall x. (a -> x) -> (b -> x)) -> (b -> a)contrayo f = f idcontrayo' ::   (b -> a) -> (forall x. (a -> x) -> (b -> x))contrayo' b2a = \a2x -> a2x . b2a

When we specialize Yoneda to b -> -, we are led to the idea that a continuation of the form (a -> x) -> (b -> x) must contain plumbing to turn bs into as: ie, it must contain a function b -> a .

-- F = id .type Id x = x-- Nat(Hom(a, -), Id - ) ~= Id a-- Nat(forall x. (a -> x), Id x) ~= Id a-- Nat(forall x. (a -> x) -> x) ~= aidyo :: (forall x. (a -> x) -> x) -> aidyo k = k ididyo' ::  a -> (forall x. (a -> x) -> x)idyo' a = \k -> k a

specializing to id recovers usual continuations.

In total, Yoneda tells us that from every enriched continuation ContF a g = Nat (Hom a) g = forall x. (a -> x) -> g x, we can recover a g a. Hence, there is a bijection between g a and ContF a g

§ Yoneda embedding

The yoneda embedding follows from the lemma. The lemma tells us that Nat(Hom(a, -), F) ~= F(a). Pick F = Hom(b, -). This gives Nat(Hom(b, -), Hom(a, -)) ~= Hom(b, a) Thus, if we consider the mapping C -> [C, Set] given by sending a to F(a), we also preseve the Hom sets as natural transformations, since Hom(b, a) is isomorphic to Nat(Hom(b, -), Hom(a, -)). Thus, we get a full and faithful embedding of the original category into the Hom category.