- 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`

- 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.