§ Yoneda Lemma and embedding

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 a
lhs2rhs 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 x
listyo :: (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 a
contrayo :: (forall x. (a -> x) -> (b -> x)) -> (b -> a)
contrayo f = f id

contrayo' ::   (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) ~= a
idyo :: (forall x. (a -> x) -> x) -> a
idyo k = k id

idyo' ::  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.