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: reading & references

Topic: closed structure in LNL adjunctions

Matteo Capucci (he/him) (Aug 01 2025 at 14:37):

Categorical semantics of linear logic commonly takes place in LNL adjunctions. Mellies' book expounds this but seem to not dwell much on the closed structure. Does anyone have a good reference where this is expounded in greater detail?

Matteo Capucci (he/him) (Aug 01 2025 at 15:33):

The following notes by @Valeria de Paiva seem a good place to start! I didn't know that categorical semantics of linear logic could be so subtle:

https://vcvpaiva.github.io/includes/pubs/catsem4all.pdf

Valeria de Paiva (Aug 01 2025 at 15:39):

Thanks for this @Matteo Capucci (he/him) !

Mike Shulman (Aug 01 2025 at 16:49):

You might be interested in my paper on LNL polycategories. Closed structures are discussed in section 2 as an instance of a general notion of universal morphism that also includes products and modalities, but I didn't dwell on them much either. I'm not sure that there's much to say by dwelling on them -- did you have specific questions?

John Baez (Aug 01 2025 at 16:50):

What does LNL stand for? :cry:

Valeria de Paiva (Aug 01 2025 at 16:51):

Linear Non Linear

Valeria de Paiva (Aug 01 2025 at 16:52):

Nick Benton's categorical model for linear logic, ie. a monoidal adjunction

Mike Shulman (Aug 01 2025 at 16:52):

I write "Linear-NonLinear" to emphasize the parsing -- an adjunction or other structure that relates a category of Linear objects to a category of NonLinear objects.

Valeria de Paiva (Aug 01 2025 at 16:55):

My point about LNL models is that they're much easier to state, but end up being as difficult to check as Linear Categories, the old model.

Valeria de Paiva (Aug 01 2025 at 16:56):

"adjunctions" are a really clever encapsulation of lots of things

Matteo Capucci (he/him) (Aug 03 2025 at 09:24):

Mike Shulman said:

You might be interested in my paper on LNL polycategories. Closed structures are discussed in section 2 as an instance of a general notion of universal morphism that also includes products and modalities, but I didn't dwell on them much either. I'm not sure that there's much to say by dwelling on them -- did you have specific questions?

Thanks Mike, I read your paper a while ago and I should revisit it with new eyes.

My specific question is understandimg what exactly ${!\multimap} = {\to}$ means, from a categorical standpoint. From Valeria's notes it seems that, given a symmetric monoidal closed category $L$ involved in a symmetric monoidal adjunction with a cartesian category $A$, the latter automatically gains a cartesian closed structure, which I guess is given by $!(A \multimap B)$ where $!$ is the right adjoint going $L \to A$. This is allegedly discussed by Barber, Benton and Plotkin but I can't find the relevant paper.
The reason I'm confused is that reading logic papers, I'm lead to believe the intuitionistic arrow $\to$ is defined for every type rather than just the 'non-linear' ones in $A$ (and $A$ can be comparatively smaller than $L$, as in the example I care about). So perhaps I'm missing something glaringly obvious (I'm no stranger to such blunders...).
This perhaps would help me better conceptualise the relationship between BI and LL...

Valeria de Paiva (Aug 03 2025 at 14:01):

@Matteo Capucci (he/him) here is the reference for Barber's thesis https://www.lfcs.inf.ed.ac.uk/reports/96/ECS-LFCS-96-347/
But you got it slightly mangled: "given a symmetric monoidal closed category $L$ involved in a symmetric monoidal adjunction with a cartesian category $A$, the latter automatically gains a cartesian closed structure", is ok. But this is not given by $!(A \multimap B)$. the intuitionistic arrow $\to$ is indeed defined for every pair of types in $A$.

Matteo Capucci (he/him) (Aug 03 2025 at 14:14):

Thanks Valeria! How is $\to$ defined then?

Matteo Capucci (he/him) (Aug 03 2025 at 14:15):

In the reference you give the cartesian category $A$ is assumed closed already

Valeria de Paiva (Aug 03 2025 at 15:54):

@Matteo Capucci (he/him) I will confess that I'm a bit rusty on this, but in page 11 of
https://scholar.google.com/scholar?&q=A.%20Barber%20and%20G.%20Plotkin%3A%20Dual%20intuitionistic%20linear%20logic.%20Submitted%20%281998%29
which was the original version of the thesis, one finds section "3.5 A Definable Intuitionistic Function Space" where Barber defines the internal-hom following Girard's original def as
A->B:= !A -o B, using a term construction, via multicategories. This might not be enough for your purposes.

Nathanael Arkor (Aug 03 2025 at 16:38):

Typically, for objects $X, Y$, the cartesian closed structure is defined by $(!X) \multimap Y$. I'm a little confused by what's written above, because it doesn't seem to type-check: you can't apply a functor to an entire category.

Valeria de Paiva (Aug 03 2025 at 18:48):

I'm using A and B as objects of the linear category.

Nathanael Arkor (Aug 03 2025 at 19:14):

Sorry, I meant what Matteo had written.

Mike Shulman (Aug 03 2025 at 19:52):

First: in the general LNL case with two classes of objects, I prefer to reserve $!$ for the induced comonad on the category of linear objects, which decomposes as $\mathord{!} = \mathsf{F} \mathsf{U}$ for the adjunction $\mathsf{F} \dashv \mathsf{U}$ between the nonlinear and linear categories.

Second: in this general situation, I don't see how one can deduce a closed structure on the entire cartesian category of nonlinear objects from having one on the monoidal category of linear objects. I can only see how to define the cartesian hom $X \to \mathsf{U}B$, where $X$ is a nonlinear object and $B$ is a linear object, the definition being $(X \to \mathsf{U}B) = \mathsf{U}(\mathsf{F}X \multimap B)$.

I believe the traditional setup, with only one class of objects, is best encoded in the general LNL context by taking $\mathsf{U}$ to be the identity on objects. In this case, the action of the comonad $!$ on objects coincides with that of $\mathsf{F}$, and so the above definition simplifies to $(X\to B) = (!X \multimap B)$. However, I find it less confusing to think about the general case, with two distinct categories each with their own objects.

Matteo Capucci (he/him) (Aug 04 2025 at 07:29):

Nathanael Arkor said:

Typically, for objects $X, Y$, the cartesian closed structure is defined by $(!X) \multimap Y$. I'm a little confused by what's written above, because it doesn't seem to type-check: you can't apply a functor to an entire category.

I messed up notation, I also meant A and B as objects in $!A \multimap B$!

Matteo Capucci (he/him) (Aug 04 2025 at 07:36):

Mike Shulman said:

I believe the traditional setup, with only one class of objects, is best encoded in the general LNL context by taking $\mathsf{U}$ to be the identity on objects. In this case, the action of the comonad $!$ on objects coincides with that of $\mathsf{F}$, and so the above definition simplifies to $(X\to B) = (!X \multimap B)$.

Indeed, this seems what logicians implicitly assume, but then I have never seen this mentioned explicitly in the categorical semantics (only exception being Seely categories where the adjunction is coKleisli, hence the right adjoint is ioo)...