• 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    / |   /  |  /   | /    va,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.