## § Natural Transformations as ends

• Ends generalize the notion of product/limit. It's sort of like an infinite product plus the wedge condition.
• $\int_X p x x$ is the notation for ends, where $p$ is a profunctor.
• Remember dimap :: (a' -> a) -> (b -> b') -> p a b -> p a' b'. Think of this as:
-----p a' b'-------
a' -> [a -> b] -> b'
--pab---

• The set of natural transformations is an end.
• Haskell: type Nat f g = forall x. f x -> g x.
• We can think of this as the "diagonal" of some end p x x for some profunctor p we need to cook up.
• type p f g a b = f a -> g b. Is p f g a profunctor?
dimap :: (a' -> a) -> (b -> b') -> (f a -> g b) -> (f a' -> g b')
dimap a'2a b2b' fa2gb = \fa' ->
let fa = fmap a'2a fa'
let gb = fa2gb fa
let gb' - fmap b2b' gb
in gb'
dimap a'2a b2b' fa2gb = (@fmap g b2b')  . fa2gb  . (@fmap f a'2a)

• Clearly, from the above implementation, we have a profunctor.
• So we have a profunctor P(a, b) = C(Fa, Gb).
• In haskell, the end is End p = forall a. p a a.
• In our notation, it's \int_x C(Fx, Gx).
• Recall the wedge condition. For a profunctor p: Cop x C -> C, and any morphism k: a -> b for a, b ∈ C, the following diagram commutes for the end \int_X p(X,X):
 (p x x, p y y, p z z, ... infinite product)
\int_x p(x,x)
/[πa]  [πb]\
v            v
p(a,a)       p(b,b)
\            /
[p(id, k)]  [p(k,id)]
\        /
v      v
p a b

• If we replace p x x with with our concrete p a b = C(fa, gb), we get:
    (forall x. f x -> g x)
/               \
[@ a]            [@ b]
v                v
τa:(f a -> g a)     τb:(f b -> g b)
\                  /
dimap id(a) k τa    dimap k id(b) τb
\                 /
\               τb.(@fmap f k): (f a-> g b)
\              /
\           COMMUTES?
\            /
(@fmap g k).τa(f a -> g b)


• This says that gk . τa = τb . fk
• But this is a naturality condition for τ!
• So every end corresponds to a natural transformation, and τ lives in [C, D](f, g).
• This shows us that the set of natural transformations can be seen as an end (?)
• I can write \int_a D(fa, ga) ~= [C, D](f, g)

#### § Invoking Yoneda

• Now, yoneda tells us that [C, Set](C(a, -), f(-)) ~= f(a).
• Now I write the above in terms of ends as \int_x Set(C(a, (x)), f(x)) ~= f(a).
• So we can write this as a "point-full" notation!
• In haskell, this would be forall x. (a -> x) -> f x ~= f a.