```
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 `x`

s.
```
-- 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 `b`

s into `a`

s: 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`

`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.