§ Ends and diagonals

• Bartosz: Wedges
• Let's think of Cop x C, and an element on the diagonal (a, a), and a function f: a -> b.
• Using the morphism (id, f), I can go from (a, a) to (a, b).
• If we have (b, b), I can once again use f to go fo (a, b).
• So we have maps:

     b,b
    / |
   /  |
  /   |
 /    v
a,a-->a,b

• This tells us that if we have something defined on the diagonal for a profunctor p a a, we can "extrapolate" to get data everywhere!
• How do we get the information about the diagonal? Well, I'm going to create a product of all the diagonal elements of the profunctor.
• so we need a limit L, along with maps L -> p c c for each c. This kind of infinite product is called a wedge (not yet, but soon).
• The terminal object in the category of wedges is the end.
• But our cone is "under-determined". We need more data at the bottom of the cone for things to cohere.
• suppose at the bottom of the cone, we want to go from p a a to p b b. for this, I need morphisms (f: b -> a, g: a -> b) to lift into the profunctor with dimap.
• We might want to impose this as coherence condition. But the problem is that there are categories where we don't have arrows going both ways (eg. partial orders).
• So instead, we need a different coherence condition. If we had a morphism from a -> b, then we can get from p a a --(id, f)-->p a b. Or, I can go from p b b --(f, id)-->p a b. The wedge condition says that these commute. So we need p id f . pi_1 = p f id . pi_2

§ Relationship to haskell

• How would we define this wedge condition in haskell?
• Because of parametricity, haskell gives us naturality for free.
• How do we define an infinite product? By propositions as types, this is the same as providing ∀x..
• End p = forall a. p a a
• We can define a cone with apex A of a diagram D: J -> C as a natural transformation cone(A): Const(A) => D. What's the version for a profunctor?
• Suppose we have a profunctor diagram P: J^op x J -> C. Then we have a constant profunctor Const(c) = \j j' -> c. Then the wedge condition (analogue of the cone condition) is to ask that we need a dinatural transformation cone': Const(A) => P.
• NOTE: a dinatural transformation is STRICTLY WEAKER than a natural transformation from J^opxJ -> C.
• Suppose we have transformation that is natural in both components. That is to say, it is a natural transfrmation of functors of the type [J^op x J -> C]. This means that we have naturality arrows α(a,b): p(a,b) -> q(a,b). Then the following must commute, for any f: a -> b by naturality of α:

      p(b,a)
    /    |
[p(f,id)]|
  /      |
p(a,a)  [α(b,a)]
 |       |
[α(a,a)] |
 |       |
 |    q(b,a)
 |     /
 |  [q(f,id)]
 |   /
q(a,a)

• Similarly, other side must commute:

      p b a
    /   |  \
[p f id]|   [p id f]
  /     |     \
p a a  [α b a] p b b
 |      |        |
[α a a] |      [α b b]
 |      |        |
 |    q b a      |
 |     /   \     |
 |  [q f id]\    |
 |   /  [q id f] |
 |  /          \ |
q a a         q b b

• I can join the two sides back together into a q a b by using [q id f] and [q f id]. The bottom square commutes because we are applying [q f id] and [q id f] in two different orders. By functoriality, this is true because to q(f.id, id.f) = q(f,f) = q(id.f, f.id).

      p b a
    /   |  \
[p f id]|   [p id f]
  /     |     \
p a a  [α b a] p b b
 |      |        |
[α a a] |      [α b b]
 |      |        |
 |    q b a      |
 |     /   \     |
 |  [q f id]\    |
 |   /  [q id f] |
 |  /          \ |
q a a         q b b
  \             /
 [q id f]      /
    \        [q f id]
     \      /
     q a b

• If we erase the central node [q b a] and keep the boundary conditions, we arrive at a diagram:

      p b a
    /      \
[p f id]    [p id f]
  /           \
p a a          p b b
 |               |
[α a a]        [α b b]
 |               |
 |               |
 |               |
 |               |
 |               |
 |               |
q a a         q b b
  \             /
 [q id f]      /
    \        [q f id]
     \      /
     q a b

• Any transformation α that obeys the above diagram is called as a dinatural transformation .
• From the above, we have proven that any honest natural transformation is a dinatural transformation, since the natural transformation obeys the diagram with the middle node.
• In this diagram, see that we only ever use α a a and α b b.
• So for well behavedness, we only need to check a dinatural transformation at the diagonal. (diagonal natural transformation?)
• so really, all I need are the diagonal maps whoch I will call α' k = α a a.
• Now, a wedge is a dinatural transformation from constant functor to this new thingie.