§ Natural Transformations as ends

• Bartosz: 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.