Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: Ends/coends and quantifiers

Nathaniel Virgo (Mar 18 2024 at 02:10):

There is a vague analogy between ends and "for all", and coends and "there exists". I would like to get a better handle on this, and while I don't have a very specific question, I'm wondering if someone here might be able to say something that can help to really pin down the intuition.

The analogy is mentioned for example in a blog post by Bartosz Milewski, but I'm not much of a programmer and don't have a great intuition about Haskell's forall keyword. So I guess I'm looking for an explanation that sort of skips the programming bit and just shows how to make the analogy between ends/coends and $\forall$/$\exists$ in logic, if the analogy is strong enough for that to make sense.

Max New (Mar 18 2024 at 02:17):

I have a paper with Dan Licata from last year that uses logical notation for working in a double category (https://link.springer.com/chapter/10.1007/978-3-031-30829-1_6) and you can interpret our uses of $\exists$ as co-ends and $\forall$ as ends. We give a few examples in section 3.

Max New (Mar 18 2024 at 02:18):

This makes a formal analogy between the two: ordinary logic and category theory are both models, so you can literally interpret the same syntax as both tautologies or categorical theorems

Max New (Mar 18 2024 at 02:22):

For instance, one of my favorites is the Yoneda lemma.

Stated in terms of an end this is
$(\int_{b} \textrm{Hom}(a, b) \to P(b)) \cong P(a)$
In this analogy, categories correspond to sets, Hom corresponds to equality, presheaves correspond to subsets and ends correspond to forall. Then if you reinterpret this in logical notation you get a very intuitive tautology:
$(\forall b. (a = b) \Rightarrow b \in P) \iff a \in P$

Max New (Mar 18 2024 at 02:26):

You can do this with e.g., Co-Yoneda as well with co-ends corresponding to existential quantifiers. I am a computer scientist so this "logical" perspective on category theory is very appealing to my intuitions

Max New (Mar 18 2024 at 02:31):

The logic we give in that paper is fairly restrictive. More generally you could have something more like a full directed higher order logic that would be the internal language of a 2-topos

Keith Elliott Peterson (Mar 18 2024 at 03:40):

I asked a similar question once.

Carrying with the above, in an enriched setting, one can view existential quantification,

$$\exists y. P(x,y),$$

as the coend,

$$\int^y P(x,y) \land \top(y,\ast).$$

Nathaniel Virgo (Mar 18 2024 at 07:54):

Ah, maybe I've got it. (Just in terms of the intuition I was trying to grasp.) I've just got to take the idea of "profunctors are like relations" literally.

Given a relation $R\subseteq X\times X$, if I view it as a profunctor between discrete categories, the end $\int_{x:X} R(x,x)$ is the set of functions $\{f:X\to R\mid f(x)=(x,x)\}$, which is the one-element set if $\forall x\in X: x\mathrel{\sim_R} x$, and the empty set otherwise. If we generalise from relations to spans this becomes something like "the set of all the ways in which it's true for all $x$", and if we generalise from spans to profunctors we're asking not only for it to be true for all $x$ but also to obey the wedge condition.

On the other hand, the coend $\int^{x:X} R(x,x)$ is the set $\{(x,y)\in R \mid x=y\}$, which is "the set of ways it's true that" $\exists x\in X: x\mathrel{\sim_R}x$. Or if I used a Bool-valued profunctor it would just mean the same as $\exists x\in X: x\mathrel{\sim_R}x$. Generalising to categories means we consider some "ways in which it's true" to be the same as others.

Peva Blanchard (Mar 18 2024 at 09:42):

Maybe another useful way (at least for me) to think about ends (and co-ends).

In a category $X$ with products and equalizers, the end of a profunctor $P : X^{op} \times X \rightarrow V$ is basically the equalizer of two arrows out of the product $\prod_{x \in X} P(x, x)$. Then, informally, the analogy "product" vs "conjunction" leads to the analogy "end" vs "universal quantifier".

Similarly, the coend is the co-equalizer of two arrows into the sum $\sum_{x \in X} P(x, x)$. So "sum" vs "disjunction" leads to "coend" vs "existential quantifier".

Cole Comfort (Mar 18 2024 at 22:53):

Here is a nice way in which they are related which I shall sketch from memory. Correct me if I make any errors.

Sets and relations form a closed linear bicategory with respect to the universal and existential composition.

Set-enriched profunctors form a closed bicategory, where the composition is given by coend and the closure is given by kan extension (I forget which).

However, if you look at quantaloid enriched profunctors, for example enriched over 2, then this is also a closed linear bicategory.... but now with respect to the end and coend. So to make the connection complete, you can't work over set enriched profunctors, but there is still a latent connection between kan extensions and entailment hanging around.

Cole Comfort (Mar 18 2024 at 23:01):

In some sense closed linear bicategories categorify *-autonomous categories, and closed bicategories categorify monoidal closed categories.

So the analogy between Rel and Set-enriched Profunctors on a structural level is similar to that between *-autonomous categories and monoidal closed categories.

John Baez (Mar 18 2024 at 23:54):

Attempting to understand Cole's remarks, I looked at [[linear bicategory]], which told me this concept was a horizontal categorification of [[linearly distributive category]]... and I was distressed to find that the latter page didn't give any examples.

John Baez (Mar 18 2024 at 23:56):

What are some good examples of linear distributive categories? So far I just know what Cole said, which is that sets and relations can be made into a linear bicategory. (I don't really understand what that means, but at least it's an example!)

Mike Shulman (Mar 19 2024 at 00:04):

Probably you mean [[linearly distributive category]]. Every [[star-autonomous category]] is linearly distributive; do you know examples of those?

John Baez (Mar 19 2024 at 00:28):

Yes... thanks. So what's an example of a linearly distributive category that's not star-autonomous?

Mike Shulman (Mar 19 2024 at 00:31):

Well, any distributive lattice that is not a Boolean algebra, with $\wedge$ and $\vee$.

Mike Shulman (Mar 19 2024 at 00:32):

Also, any monoidal category with $\otimes = ⅋$.

Mike Shulman (Mar 19 2024 at 00:33):

Less trivial examples are harder to come by, I'm not thinking of one off the top of my head.

Mike Shulman (Mar 19 2024 at 00:38):

Oh, the original Cockett-Seely paper has another example: if $D$ is an invertible object in a monoidal category, then $X ⅋ Y = X \otimes D \otimes Y$ defines a linearly distributive category whose linear distributors are isomorphisms.

Mike Shulman (Mar 19 2024 at 00:40):

Also, they say, the category of modules of a bialgebra in any $\ast$-autonomous category, or even in any linearly distributive category, is linearly distributive, and generally only $\ast$-autonomous if the bialgebra is a Hopf algebra.

Mike Shulman (Mar 19 2024 at 00:44):

I added these to the nLab!

Cole Comfort (Mar 19 2024 at 01:33):

John Baez said:

Attempting to understand Cole's remarks, I looked at [[linear bicategory]], which told me this concept was a horizontal categorification of [[linearly distributive category]]... and I was distressed to find that the latter page didn't give any examples.

The way I am thinking of this connection, if it categorifies properly is in terms of @Mike Shulman 's result that says you can always embed a symmetric monoidal closed category within a *-autonomous category. So that the bubble and clasp way of currying things can always be pulled apart by adding more objects and obtaining another tensor product, where the monoidal closure be represented by linear adjunctions.

In quantaloid enriched profunctors the "end" and "coend" categorify tensor and par. In Rel, the universal quantifier and the existential quantifier categorify tensor and par. But if you work in set enriched profunctors, then you still have the categorification of monoidal closure, which is given by kan extension. In Rel, this corresponds to entailment. But the end does not give you a bicategory structure here, even though it can be used to construct the kan extension. It is possible that there is some categorification of @Mike Shulman 's conservativity result, which allows you to extend Prof to a linear bicategory in a way, but this is purely speculation.

Mike Shulman (Mar 19 2024 at 03:14):

I think I don't understand your original comment. $V$-enriched profunctors, for any complete and cocomplete closed monoidal category $V$, form a closed bicategory. This includes sets and relations, sets and set-profunctors, and quantaloid-enriched profunctors. The composition in all cases is given by coends, while the adjoint internal-homs are given by ends. I don't know about any linear-bicategory structure, but it doesn't seem necessary to me here.

Cole Comfort (Mar 19 2024 at 08:57):

Mike Shulman said:

I think I don't understand your original comment. $V$-enriched profunctors, for any complete and cocomplete closed monoidal category $V$, form a closed bicategory. This includes sets and relations, sets and set-profunctors, and quantaloid-enriched profunctors. The composition in all cases is given by coends, while the adjoint internal-homs are given by ends. I don't know about any linear-bicategory structure, but it doesn't seem necessary to me here.

What is the $V$ such that $\sf Rel$ is given by $V$-enriched profunctors? I wasn't aware it could be constructed that way.

My point about the linear bicategory structure is that in these cases it allows you to compose two morphisms with the end/universal quantifier, just as you would normally with the coend/existential quantifier. So in my view this is a big difference between $\sf Prof$ and $\sf Rel$. Because having this notion of composition is stronger than adjoint internal homs.

Mike Shulman (Mar 19 2024 at 14:59):

Yes, that's true, Rel is only a full sub-bicategory of Bool-Prof, sorry. But that's enough to make it closed.

Mike Shulman (Mar 19 2024 at 15:02):

I see what you're saying about the linear bicategory structure. But I don't see how you get such a structure for profunctors over a quantaloid; don't you need the base of enrichment to also be $\ast$-autonomous?

Cole Comfort (Mar 19 2024 at 15:36):

Oh yes, I misremembered what is proven in this paper:
https://arxiv.org/pdf/2209.05693.pdf

You actually need the base of enrichment to be a Girard quantaloid, or a Girard quantale, which I think addresses this.

It has kind of bothered me for a while that $\sf Prof$ doesn't have this structure, because it is contrary to my intuition which I have developed by working with relations.

Cole Comfort (Mar 19 2024 at 15:49):

The only base of enrichment have been thinking of other than $\sf Set$ is $\sf Bool$, which is pretty much as degenerate as it gets, and I think has all of this structure for trivial reasons.

Mike Shulman (Mar 19 2024 at 16:17):

Ah, yes: a symmetric quantale is Girard precisely when it is $\ast$-autonomous, and a non-symmetric one is some kind of cyclic non-symmetric $\ast$-autonomous poset.

Mike Shulman (Mar 19 2024 at 16:18):

On the other hand, the only reason Rel itself has this structure is because your underlying logic is classical! If you work with relations in a more general topos, it won't be linear.

Cole Comfort (Mar 19 2024 at 17:13):

Do you mean linear in the "linear bicategory" sense? I have done lots of work with relations internal to finite dimensional vector spaces (linear relations), and this linear bicategory structure doesn't exist there. Maybe that is one explanation for why.

Mike Shulman (Mar 19 2024 at 18:02):

Yes, that sense of linear. (I'm not really a fan of the terminology "linear bicategory", but I haven't heard any good suggestions for a replacement.)