Assume the category C is *-autonomous. We can define ⊥ = 1* and a ⊕ b = (a* ⊗ b*)* for all a, b ∈ C. Further, by assumption there is an isomorphism

C(a ⊗ b, c*) ≅ C(a, (b ⊗ c)*), for all a, b, c ∈ C.

I think I got the definition of the (co)evaluation morphisms themselves. For example, for x ∈ C we can set a = x*, b = x, and c = 1 = ⊥* to obtain C(x* ⊗ x, ⊥) ≅ C(x*, x*) and so we can define the evaluation of x as the retract of the identity. However, I don't understand why this implies that the snake identities follow. The coherence relations for linearly distributive categories with negation are framed in terms of the δ^{R,L}_{R,L}'s, which say that the tensor products are strong with respect to each other. Is the idea that, starting from a *-autonomous category, we can define these morphisms in such a way so that this follows automatically? Is this perhaps written down somewhere?

As a corollary: on the star-autonomous category page it says that they are rigid when there is a natural isomorphism from (a ⊗ b)* to a* ⊗ b*. However, if the above is true, isn't it the case that we rather require the dualising functor to be a certain kind of monoidal functor (i.e., the isomorphism from (a ⊗ b)* to a* ⊗ b* has to be a particular one)? Otherwise, on objects we would have that a ⊗ b ≅ a ⊕ b, but since the associators would be different (I guess?), the "regular" snake identities that we required for rigidity still wouldn't follow.

Am I missing something?

Best,

Tony Zorman (TU Dresden) ]]>

Okay, thanks – all that makes sense. Robin would be in a position to know I think.

]]>My guess is that Revision 5 was the outcome of the merger Urs made described at the following link.

https://nforum.ncatlab.org/discussion/6517/weakly-distributive-category/

If so, I’d guess that Robin Cockett is the author.

]]>I don’t remember writing this, nor do I know half of what it’s saying. If it was me who entered this into the entry, it must have been in helping somebody else get their comment into the $n$Lab. This must have been written by somebody with inside knowledge of the linear logic community – not me. Maybe this was a contribution to another forum or blog, and was thought to deserve to be archived on the $n$Lab. Feel free to edit as need be.

]]>Looks to me like that phrase was added in revision 5 by Urs.

]]>Dating back to revision 8 (Mike Shulman): “At that time this was generally thought to be a rather unsatisfactory and unnecessarily technical solution especially when compared to the normal forms to which the community was accustomed.”

Not that I’m doubting this, but it’s the first time I’m learning about it. Any citations?

]]>Added more historical notes. Added and tidied up references.

Rongmin Lu

]]>I’ve added a small historical correction.

]]>Actually, I now realized that there are actually *three* different notions of functor between linearly distributive category that appear in the literature: the Cockett-Seely “linear functors”, the linear functors whose $\otimes$-part and $\parr$-part agree as functors (which I’m tempted to call “Frobenius linear functors”), and the ones that moreover are *strong* monoidal for both structures. The “$\ast$-autonomous nucleus” of a linearly distributive category uses “linear functors”, whereas the free linearly distributive category on a polycategory uses strong Frobenius linear functors. Which notion of functor is the free $\ast$-autonomous category on a linearly distributive category (#16 above) free with respect to? I’m guessing also the strong Frobenius ones?

I added a sketch definition of the 2-category of linearly distributive categories, and a remark that the forgetful functor from $\ast$-autonomous ones to linearly distributive ones also has a *right* adjoint. I also uniformized the notation on the page to $(\otimes,\top)$ and $(\parr,\bot)$ for the monoidal structures; I hope no one objects to that.

One reason ordinary dual objects are interesting is that they allow us to define traces. With the “unit” and “counit” defined using different monoidal structures in a $\ast$-autonomous category, we can’t define a trace in the usual way. But this problem is somewhat reminiscent to me of what happens with bicategorical traces, so I wonder whether it has a similar solution. If we equip a $\ast$-autonomous category $C$ with a functor $sh:C\to D$ and isomorphisms $sh(A\otimes B) \cong sh(A\parr B)$, then we could define the trace of any endomorphism $f:A\to A$ to be the composite

$sh(\top) \to sh(A\parr A^*) \xrightarrow{f} sh(A\parr A^*) \cong sh(A^* \parr A) \cong sh(A^* \otimes A) \to sh(\bot)$I wonder whether there are any interesting examples of this?

]]>Thanks for taking the time to help me understand all this, by the way.

]]>I added some more remarks to linearly distributive category and star-autonomous category based on this discussion.

]]>Nice. I should have read that paper more carefully.

One other reason the notion of linearly distributive category is difficult for me is that it isn’t usually “packaged” in a categorically nice way, making it seem somewhat *ad hoc*. For instance, the notion of duoidal category seems a little weird when written out explicitly, but it makes more sense when you say that it’s just a pseudomonoid in the 2-category of monoidal categories and lax monoidal functors. The observation about tensorial strength is partway to the sort of thing I would like to say, but it doesn’t describe the structure completely.

Here’s a first attempt. If $C$ is any monoidal category, then there is a 2-category of (pseudo) $C$-modules (which I guess some people call “actegories”) and lax $C$-module morphisms. As noted at the page tensorial strength, we can regard $C$ as a $C$-module, and in this case the lax $C$-module maps $C\to C$ are precisely the tensorially-strong endofunctors. Now in fact, at least if $C$ is symmetric, then the 2-category of $C$-modules should be a *2-multicategory*, where the multimorphisms are “lax in each variable separately”. One might then hope that a symmetric linearly distributive category is precisely a symmetric monoidal category $(C,\otimes)$ together with the structure $\parr$ of a symmetric pseudomonoid in this 2-multicategory on $C$ regarded as a $C$-module. However, this doesn’t seem quite right; I can’t see how to get out of it the “distribution and distribution” axiom in Cockett-Seely. Does it follow somehow? Or can one modify this definition so as to be able to get it out?

Ah, I take it back: Cockett-Seely, 5.3 and 5.4, specify that linearly distributive categories where the distributivities are isomorphisms are the same as “shifted” (symmetric) monoidal categories. If I’m not mistaken, supervector spaces provides an instructive example of this.

]]>Yes, exactly.

I’m pretty sure that if those constraints are isomorphisms, then the monoidal structures coincide. I should work this out more explicitly to satisfy myself, but this should be related to Brian Day’s result that when one localizes the free symmetric monoidal closed category on a symmetric monoidal category with respect to the strength constraints $(A \multimap B) \otimes C \to A \multimap (B \otimes C)$ (i.e., forcing them to be isomorphisms), then you get the free compact closed category on the symmetric monoidal category. That strength constraint corresponds to the linear distributivity.

]]>Ah, I see! Somehow that makes $\ast$-autonomous categories and linearly distributive categories make some more sense to me: a $\ast$-autonomous category is one which is almost compact closed, but where the unit and counit of the “dualities” use different monoidal structures; and a linearly distributive category is one with two monoidal structures that interact in exactly the way that’s necessary for this to make sense.

Does it ever happen nontrivially (i.e. apart from the case where the two monoidal structures coincide) that the distributors in a linearly distributive category are isomorphisms?

]]>The free $\ast$-autonomous category on a linearly distributive category is formed by adjoining (in the doctrine of linearly distributive categories) objects $\neg A$ and arrows

$\top \to A \parr \neg A, \qquad \neg A \otimes A \to \bot$subject to triangular equations

$1_A = \left( A \cong \top \otimes A \to (A \parr \neg A) \otimes A \stackrel{dist}{\to} A \parr (\neg A \otimes A) \to A \parr \bot \cong A \right)$ $\,$ $1_{\neg A} = \left( \neg A \cong \neg A \otimes \top \to \neg A \otimes (A \parr \neg A) \stackrel{dist}{\to} (\neg A \otimes A) \parr \neg A \to \bot \parr \neg A \cong \neg A \right)$and where we have $\parr = \otimes, \bot = \top$, this is exactly how one would form the free compact closed category generated by the symmetric monoidal category $C$.

This construction is mentioned both in the original Cockett-Seely paper (page 159 ff) and in Blute-Cockett-Seely-Trimble.

By the way, that Cockett-Seely paper also handily spells out the definition of polycategories (which is due to Manfred Szabo); someone should just copy that over to the nLab (and that someone could be me).

]]>Interesting; that will take some thought. Can you give any intuition for why the free $\ast$-autonomous category on a symmetric monoidal category *qua* linearly distributive category would coincide with the free compact closed category?

I don’t know an answer to 1 off hand. But the lack of such might be related to an observation below.

The free $\ast$-autonomous category in this case would coincide with the free compact closed category. From a sequent calculus perspective, this is (I think) a weird case because IIRC there’s no good cut-elimination procedure. (Notice that string-theoretically, composition can produce loops or islands, which in the case of free compact closed categories on a category $C$, must be accounted for by taking the trace of a category $C$. Meanwhile loops don’t occur in a cut-free fragment, unless perhaps they are put in by hand as axioms, for each $C$.)

I am not aware of any really clean way of describing the free compact closed category on a symmetric monoidal category. The free compact closed category $F(C)$ on a category $C$ has I think a halfway decent description in terms of a kind of wreath product $F(1) \wr C$ where edges of graphs in $F(1)$ are labeled by morphisms in $C$ (and loops by elements of $tr(C)$). If $S(C)$ is the free symmetric monoidal category on $C$, then I guess the relatively free compact closed category on a symmetric monoidal category $C$ can be formed as a suitable kind of 2-colimit (a co-isoinserter? not sure) of a diagram of type

$F S C \rightrightarrows F C$which could be further described by applying rewrite rules on morphisms of $F C$, but I’m not sure such rewrite rules can be organized nicely.

]]>Great. I added that to the page. Two related questions:

Do you know whether anyone has written down a type theory for “symmetric monoidal categories regarded as linearly distributive”? I’m imagining a sequent calculus with multiple formulas in both antecedent and consequent, and where you’re allowed to cut on multiple formulas at once.

What is the free $\ast$-autonomous category on a symmetric monoidal category regarded as linearly distributive? Does it have a nice description?

Yes, all the required structure and coherence conditions follow straight from coherence for symmetric monoidal categories.

]]>Is it true that any symmetric monoidal category is linearly distributive (but not, of course, $\ast$-autonomous) if we define $\parr = \otimes$?

]]>Feel free to brush it up. (-: If what you’re worried about is that polycategories don’t have connectives, then maybe “…for the judgmental structure of classical linear logic”?

]]>