• 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            vp(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.