Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorMike Shulman
   • CommentTimeMay 11th 2016
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI reorganized [[linearly distributive category]] by moving the long block of history down to the bottom, adding an "Idea" section and a description of how $*$-autonomous categories give rise to linearly distributive ones and linearly distributive ones give rise to polycategories. I also cross-linked the page better with [[polycategory]] and [[star-autonomous category]].

   I reorganized linearly distributive category by moving the long block of history down to the bottom, adding an “Idea” section and a description of how $*$-autonomous categories give rise to linearly distributive ones and linearly distributive ones give rise to polycategories. I also cross-linked the page better with polycategory and star-autonomous category.

2. • CommentRowNumber2.
   • CommentAuthorTodd_Trimble
   • CommentTimeMay 12th 2016
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexThanks, Mike! It should be pointed out that at least some of those coherence conditions are essentially [[tensorial strength]] conditions (noting that each of those $\delta$'s, read as strengths, can be read either as $\otimes$-ing with $A$ is strong over $\wp$, or $\wp$-ing with $A$ is strong over $\otimes$).

   Thanks, Mike!

   It should be pointed out that at least some of those coherence conditions are essentially tensorial strength conditions (noting that each of those $\delta$’s, read as strengths, can be read either as $\otimes$-ing with $A$ is strong over $\wp$, or $\wp$-ing with $A$ is strong over $\otimes$).

3. • CommentRowNumber3.
   • CommentAuthorMike Shulman
   • CommentTimeMay 12th 2016
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexFeel free to add that to the page... (-:

   Feel free to add that to the page… (-:

4. • CommentRowNumber4.
   • CommentAuthorMike Shulman
   • CommentTimeMay 12th 2016
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexThe notion of linearly distributive category is not very intuitive to me, particularly as regards these constructions. I mean, looking at the definition of star-autonomous category, I don't "see" a linearly distributive category underneath --- heck, the definition doesn't even include $\parr$ --- and looking at the definition of linearly distributive category, I don't "see" a polycategory underneath. Maybe I just need to practice to improve my vision, but if anyone can provide some extra intuition I wouldn't mind.

   The notion of linearly distributive category is not very intuitive to me, particularly as regards these constructions. I mean, looking at the definition of star-autonomous category, I don’t “see” a linearly distributive category underneath — heck, the definition doesn’t even include $\parr$ — and looking at the definition of linearly distributive category, I don’t “see” a polycategory underneath. Maybe I just need to practice to improve my vision, but if anyone can provide some extra intuition I wouldn’t mind.

5. • CommentRowNumber5.
   • CommentAuthorTodd_Trimble
   • CommentTimeMay 12th 2016
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexI don't know that I can help much, Mike. But usually I revert back to $\ast$-autonomous categories, knowing that every linearly distributive category (aka "weakly distributive category" back in the day) comes canonically from a $\ast$-autonomous category: if $C$ is linearly distributive then the unit $C \to U F C$ is an equivalence of linearly distributive categories, where $F \dashv U: \ast-Auton \to LinDist$ is the free-forgetful adjunction. (Linear logic is a conservative extension of the $(\otimes, \parr)$-fragment.) From that point of view, the strengths just come from a corresponding strength for $\ast$-autonomous categories, e.g., $a^b \otimes c \to (a \otimes c)^b$ where $a^b$ is alternate shorthand for $b \multimap a$. (A fact that is useful: if $V$ is symmetric monoidal closed, then any unary functor $V \to V$ definable in the language of smc categories carries a canonical strength, in fact a unique strength by the coherence for smc categories. This extends to the case where we include *contravariant* functors $V \to V$ along with the covariant ones, although the notion of tensorial strength for contravariant functors might not be as well-known as for covariant ones.) As for seeing the polycategory underneath, I guess you know that linearly distributive categories were invented in the first place to explain what polycategories are from the viewpoint of categorical algebra. You yourself wrote the blurb on how you get a polycategory out of a linearly distributive category (so again I don't know I can help much further), but again, my tendency is to think directly in terms of linear logic and $\ast$-autonomous categories, where we know how to interpret two-sided sequents $A_1, \ldots, A_m \to B_1, \ldots, B_n$. Thus, if you can see an underlying polycategory in a $\ast$-autonomous category (or if you know how to build a $\ast$-autonomous freely out of two-sided sequents), then you can in a linearly distributive category (more directly in fact, since we cut out the linear $\neg$ middleman). By the way, I wouldn't say that polycategories are a "natural categorical semantics" for linearly distributive categories [1] -- if I'd say anything along these lines, I'd say that's backwards: it's more that linearly distributive categories provide categorical semantics for polycategories! But even that is not how I'd put it. Normally one refers to categorical semantics of various fragments of (e.g. propositional) logic, so I'd really rather say that linearly distributive categories provide a semantics for the multiplicative conjunction and disjunction fragment of (linear) logic. Polycategories are actually slightly alien from the viewpoint of category theory, since we cut at only one formula at a time, but linearly distributive categories is how a category theorist might make sense of them. [1] In fact I think it's just wrong to say polycategories are a semantics for ld categories or for the $(\otimes, \parr)$-fragment, since general polycategories don't interpret formulas $A \otimes B, A \parr B$.

   I don’t know that I can help much, Mike. But usually I revert back to $\ast$-autonomous categories, knowing that every linearly distributive category (aka “weakly distributive category” back in the day) comes canonically from a $\ast$-autonomous category: if $C$ is linearly distributive then the unit $C \to U F C$ is an equivalence of linearly distributive categories, where $F \dashv U: \ast-Auton \to LinDist$ is the free-forgetful adjunction. (Linear logic is a conservative extension of the $(\otimes, \parr)$-fragment.)

   From that point of view, the strengths just come from a corresponding strength for $\ast$-autonomous categories, e.g., $a^b \otimes c \to (a \otimes c)^b$ where $a^b$ is alternate shorthand for $b \multimap a$. (A fact that is useful: if $V$ is symmetric monoidal closed, then any unary functor $V \to V$ definable in the language of smc categories carries a canonical strength, in fact a unique strength by the coherence for smc categories. This extends to the case where we include contravariant functors $V \to V$ along with the covariant ones, although the notion of tensorial strength for contravariant functors might not be as well-known as for covariant ones.)

   As for seeing the polycategory underneath, I guess you know that linearly distributive categories were invented in the first place to explain what polycategories are from the viewpoint of categorical algebra. You yourself wrote the blurb on how you get a polycategory out of a linearly distributive category (so again I don’t know I can help much further), but again, my tendency is to think directly in terms of linear logic and $\ast$-autonomous categories, where we know how to interpret two-sided sequents $A_1, \ldots, A_m \to B_1, \ldots, B_n$. Thus, if you can see an underlying polycategory in a $\ast$-autonomous category (or if you know how to build a $\ast$-autonomous freely out of two-sided sequents), then you can in a linearly distributive category (more directly in fact, since we cut out the linear $\neg$ middleman).

   By the way, I wouldn’t say that polycategories are a “natural categorical semantics” for linearly distributive categories [1] – if I’d say anything along these lines, I’d say that’s backwards: it’s more that linearly distributive categories provide categorical semantics for polycategories! But even that is not how I’d put it. Normally one refers to categorical semantics of various fragments of (e.g. propositional) logic, so I’d really rather say that linearly distributive categories provide a semantics for the multiplicative conjunction and disjunction fragment of (linear) logic. Polycategories are actually slightly alien from the viewpoint of category theory, since we cut at only one formula at a time, but linearly distributive categories is how a category theorist might make sense of them.

   [1] In fact I think it’s just wrong to say polycategories are a semantics for ld categories or for the $(\otimes, \parr)$-fragment, since general polycategories don’t interpret formulas $A \otimes B, A \parr B$.

6. • CommentRowNumber6.
   • CommentAuthorMike Shulman
   • CommentTimeMay 12th 2016
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexDid I say that polycategories are a categorical semantics for linearly distributive categories? I agree that that makes no sense --- categorical structures are categorical semantics for *logic*, not for each other. If that's on one of the pages it should be fixed. Richard Garner's approach to polycategories (cited on the page now) describes them with a "multi-object cut" in terms of a pseudo-distributive law. In fact I think there is a theory of "generalized polycategories" analogous to "generalized multicategories" but as far as I know no one has written it down yet. Regarding intuition, to be honest I still struggle with all three of these structures on their own, even before thinking about how they relate to each other. The cut rule for linear logic is still strange to me, possibly coming down to the meaning of $\parr$ again --- how can you have a "disjunction" where you don't know which of the disjuncts is true, but nevertheless you somehow have to "use up the resources" involved in *all* of them? Possibly what I need to do is spend more time with concrete examples like Chu constructions.

   Did I say that polycategories are a categorical semantics for linearly distributive categories? I agree that that makes no sense — categorical structures are categorical semantics for logic, not for each other. If that’s on one of the pages it should be fixed.

   Richard Garner’s approach to polycategories (cited on the page now) describes them with a “multi-object cut” in terms of a pseudo-distributive law. In fact I think there is a theory of “generalized polycategories” analogous to “generalized multicategories” but as far as I know no one has written it down yet.

   Regarding intuition, to be honest I still struggle with all three of these structures on their own, even before thinking about how they relate to each other. The cut rule for linear logic is still strange to me, possibly coming down to the meaning of $\parr$ again — how can you have a “disjunction” where you don’t know which of the disjuncts is true, but nevertheless you somehow have to “use up the resources” involved in all of them? Possibly what I need to do is spend more time with concrete examples like Chu constructions.

7. • CommentRowNumber7.
   • CommentAuthorTodd_Trimble
   • CommentTimeMay 12th 2016
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexNo, you didn't say that. But it's on the [[polycategory]] page (sorry not to have specified that earlier). Now that you mention Richard Garner, I vaguely remember that Robin Houston also had a neat way of thinking about polycategories or $\ast$-autonomous categories, which I'll try to recall when I have some time. There are some good examples of linearly distributive categories on the [[star-autonomous category]] page, so that might be worth a look. However, another source of intuition though is proof nets. Is that something you've played with? The validity criterion for proof nets relies crucially on the structure of $\parr$-connectives (meaning instances of $\parr$ when looking at positive formulas, i.e., formulas of $\Delta$ on the right of a sequent $\Gamma \to \Delta$, or instances of $\otimes$ when looking at negative formulas, i.e., formulas of $\Gamma$). I should really spend some time writing some of this up at the nLab, because it's closely connected with my PhD thesis. In the meantime, you might also benefit from reading Girard's original article Linear Logic and especially where he gets into proof nets and his "cyclic trips" and his longtrip criterion, which is the kind of thing I'm alluding to in the previous paragraph. A more streamlined approach to proof nets was later given by Danos and Regnier. But in a nutshell, to decide whether a proof structure on a sequent $ \to \Gamma$ is a proof net (is derivable in the theory of say $\ast$-autonomous categories or linearly distributive categories), the criterion is basically that for all the $2^n$ ways of setting switches at the $n$ $\parr$-connectives occurring in subformulas of $\Gamma$, the result is an acyclic connected graph -- a tree. (For the moment I'm considering only those $\Gamma$ in which monoidal units do not appear -- how to handle units requires an extension which was a major part of my thesis.) Bah -- I'm doing a terrible job trying to discuss this here. So much to say. I'd better spend some time in the Lab and organize my thoughts there, and when I come back up for some air, maybe we can discuss this further.

   No, you didn’t say that. But it’s on the polycategory page (sorry not to have specified that earlier).

   Now that you mention Richard Garner, I vaguely remember that Robin Houston also had a neat way of thinking about polycategories or $\ast$-autonomous categories, which I’ll try to recall when I have some time.

   There are some good examples of linearly distributive categories on the star-autonomous category page, so that might be worth a look. However, another source of intuition though is proof nets. Is that something you’ve played with? The validity criterion for proof nets relies crucially on the structure of $\parr$-connectives (meaning instances of $\parr$ when looking at positive formulas, i.e., formulas of $\Delta$ on the right of a sequent $\Gamma \to \Delta$, or instances of $\otimes$ when looking at negative formulas, i.e., formulas of $\Gamma$).

   I should really spend some time writing some of this up at the nLab, because it’s closely connected with my PhD thesis. In the meantime, you might also benefit from reading Girard’s original article Linear Logic and especially where he gets into proof nets and his “cyclic trips” and his longtrip criterion, which is the kind of thing I’m alluding to in the previous paragraph. A more streamlined approach to proof nets was later given by Danos and Regnier.

   But in a nutshell, to decide whether a proof structure on a sequent $\to \Gamma$ is a proof net (is derivable in the theory of say $\ast$-autonomous categories or linearly distributive categories), the criterion is basically that for all the $2^n$ ways of setting switches at the $n$ $\parr$-connectives occurring in subformulas of $\Gamma$, the result is an acyclic connected graph – a tree. (For the moment I’m considering only those $\Gamma$ in which monoidal units do not appear – how to handle units requires an extension which was a major part of my thesis.)

   Bah – I’m doing a terrible job trying to discuss this here. So much to say. I’d better spend some time in the Lab and organize my thoughts there, and when I come back up for some air, maybe we can discuss this further.

8. • CommentRowNumber8.
   • CommentAuthorMike Shulman
   • CommentTimeMay 12th 2016
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI don't see it on the polycategory page either; what I see under "Internal logic" is "Polycategories provide a natural categorical semantics for linear logic." I've looked at proof nets a little, a while ago, but I don't think they really help; it seems to me just a way of reformulating the confusing thing that doesn't make it any less confusing.

   I don’t see it on the polycategory page either; what I see under “Internal logic” is “Polycategories provide a natural categorical semantics for linear logic.”

   I’ve looked at proof nets a little, a while ago, but I don’t think they really help; it seems to me just a way of reformulating the confusing thing that doesn’t make it any less confusing.

9. • CommentRowNumber9.
   • CommentAuthorTodd_Trimble
   • CommentTimeMay 12th 2016
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexOops. So it does. My bad (although I still think that sentence needs to be brushed up a little).

   Oops. So it does. My bad (although I still think that sentence needs to be brushed up a little).

10. • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeMay 12th 2016
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexFeel 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"?

    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”?

11. • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeMay 13th 2016
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexIs it true that any symmetric monoidal category is linearly distributive (but not, of course, $\ast$-autonomous) if we define $\parr = \otimes$?

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

12. • CommentRowNumber12.
    • CommentAuthorTodd_Trimble
    • CommentTimeMay 13th 2016
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexYes, all the required structure and coherence conditions follow straight from coherence for symmetric monoidal categories.

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

13. • CommentRowNumber13.
    • CommentAuthorMike Shulman
    • CommentTimeMay 13th 2016
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexGreat. I added that to the page. Two related questions: 1. 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. 2. What is the free $\ast$-autonomous category on a symmetric monoidal category regarded as linearly distributive? Does it have a nice description?

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

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

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

14. • CommentRowNumber14.
    • CommentAuthorTodd_Trimble
    • CommentTimeMay 14th 2016
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexI 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.

    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.

15. • CommentRowNumber15.
    • CommentAuthorMike Shulman
    • CommentTimeMay 14th 2016
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexInteresting; 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?

    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?

16. • CommentRowNumber16.
    • CommentAuthorTodd_Trimble
    • CommentTimeMay 14th 2016
    • (edited May 14th 2016)
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexThe 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](http://www.sciencedirect.com/science/article/pii/0022404995001603) (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).

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

17. • CommentRowNumber17.
    • CommentAuthorMike Shulman
    • CommentTimeMay 14th 2016
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexAh, 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?

    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?

18. • CommentRowNumber18.
    • CommentAuthorTodd_Trimble
    • CommentTimeMay 14th 2016
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexYes, 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.

    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.

19. • CommentRowNumber19.
    • CommentAuthorTodd_Trimble
    • CommentTimeMay 15th 2016
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexAh, I take it back: [Cockett-Seely](http://www.sciencedirect.com/science/article/pii/0022404995001603), 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.

    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.

20. • CommentRowNumber20.
    • CommentAuthorMike Shulman
    • CommentTimeMay 15th 2016
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexNice. 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?

    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?

21. • CommentRowNumber21.
    • CommentAuthorMike Shulman
    • CommentTimeMay 15th 2016
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexI added some more remarks to [[linearly distributive category]] and [[star-autonomous category]] based on this discussion.

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

22. • CommentRowNumber22.
    • CommentAuthorMike Shulman
    • CommentTimeMay 15th 2016
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexThanks for taking the time to help me understand all this, by the way.

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

23. • CommentRowNumber23.
    • CommentAuthorMike Shulman
    • CommentTimeMay 18th 2016
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexOne 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](http://arxiv.org/abs/0910.1306), 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?

    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?

24. • CommentRowNumber24.
    • CommentAuthorMike Shulman
    • CommentTimeOct 20th 2017
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexI 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.

    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.

25. • CommentRowNumber25.
    • CommentAuthorMike Shulman
    • CommentTimeOct 20th 2017
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexActually, 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?

    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?

26. • CommentRowNumber26.
    • CommentAuthorvaleriadepaiva
    • CommentTimeJul 30th 2021
    • PermaLink
    Author: valeriadepaiva
    Format: MarkdownItexI've added a small historical correction. <a href="https://ncatlab.org/nlab/revision/diff/linearly+distributive+category/20">diff</a>, <a href="https://ncatlab.org/nlab/revision/linearly+distributive+category/20">v20</a>, <a href="https://ncatlab.org/nlab/show/linearly+distributive+category">current</a>

    I’ve added a small historical correction.

    diff, v20, current

27. • CommentRowNumber27.
    • CommentAuthornLab edit announcer
    • CommentTimeJul 31st 2021
    • PermaLink
    Author: nLab edit announcer
    Format: MarkdownItexAdded more historical notes. Added and tidied up references. Rongmin Lu <a href="https://ncatlab.org/nlab/revision/diff/linearly+distributive+category/21">diff</a>, <a href="https://ncatlab.org/nlab/revision/linearly+distributive+category/21">v21</a>, <a href="https://ncatlab.org/nlab/show/linearly+distributive+category">current</a>

    Added more historical notes. Added and tidied up references.

    Rongmin Lu

    diff, v21, current

28. • CommentRowNumber28.
    • CommentAuthorTodd_Trimble
    • CommentTimeAug 2nd 2021
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexDating 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?

    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?

29. • CommentRowNumber29.
    • CommentAuthorMike Shulman
    • CommentTimeAug 3rd 2021
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexLooks to me like that phrase was added in [revision 5](https://ncatlab.org/nlab/revision/diff/linearly+distributive+category/5) by Urs.

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

30. • CommentRowNumber30.
    • CommentAuthorUrs
    • CommentTimeAug 3rd 2021
    • PermaLink
    Author: Urs
    Format: MarkdownItexI 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.

    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.

31. • CommentRowNumber31.
    • CommentAuthorRichard Williamson
    • CommentTimeAug 3rd 2021
    • (edited Aug 3rd 2021)
    • PermaLink
    Author: Richard Williamson
    Format: MarkdownItexMy 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/](https://nforum.ncatlab.org/discussion/6517/weakly-distributive-category/) If so, I'd guess that Robin Cockett is the author.

    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.

32. • CommentRowNumber32.
    • CommentAuthorTodd_Trimble
    • CommentTimeAug 4th 2021
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexOkay, thanks -- all that makes sense. Robin would be in a position to know I think.

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

33. • CommentRowNumber33.
    • CommentAuthorGuest
    • CommentTimeOct 22nd 2022
    • PermaLink
    Author: Guest
    Format: TextI have a (perhaps naïve) question regarding *-autonomy and linear distributivity. On the page, it says that *-autonomous categories are the same as linear distributive categories with negation, with a citation to "Weakly Distributive Categories". However, while it's clear to me how one would obtain a linear distributive structure (going much along the lines of the outlined example in the paper), I fail to see how we can obtain the right kind of negation; more specifically, why the "snake identities" (or rather, analogues for linear distributive categories, as they appear in the paper) hold. 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)

    I have a (perhaps naïve) question regarding *-autonomy and linear distributivity. On the page, it says that *-autonomous categories are the same as linear distributive categories with negation, with a citation to "Weakly Distributive Categories". However, while it's clear to me how one would obtain a linear distributive structure (going much along the lines of the outlined example in the paper), I fail to see how we can obtain the right kind of negation; more specifically, why the "snake identities" (or rather, analogues for linear distributive categories, as they appear in the paper) hold.
    
    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)
34. • CommentRowNumber34.
    • CommentAuthorMike Shulman
    • CommentTimeMar 19th 2024
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexAdded a section on examples. <a href="https://ncatlab.org/nlab/revision/diff/linearly+distributive+category/23">diff</a>, <a href="https://ncatlab.org/nlab/revision/linearly+distributive+category/23">v23</a>, <a href="https://ncatlab.org/nlab/show/linearly+distributive+category">current</a>

    Added a section on examples.

    diff, v23, current

35. • CommentRowNumber35.
    • CommentAuthornLab edit announcer
    • CommentTime5 days ago
    • PermaLink
    Author: nLab edit announcer
    Format: MarkdownItexFixed the types for linear natural transformations Priyaa Srinivasan <a href="https://ncatlab.org/nlab/revision/diff/linearly+distributive+category/24">diff</a>, <a href="https://ncatlab.org/nlab/revision/linearly+distributive+category/24">v24</a>, <a href="https://ncatlab.org/nlab/show/linearly+distributive+category">current</a>

    Fixed the types for linear natural transformations

    Priyaa Srinivasan

    diff, v24, current

36. • CommentRowNumber36.
    • CommentAuthornLab edit announcer
    • CommentTime5 days ago
    • PermaLink
    Author: nLab edit announcer
    Format: MarkdownItexAdded reference to linear bicategories Priyaa Srinivasan <a href="https://ncatlab.org/nlab/revision/diff/linearly+distributive+category/24">diff</a>, <a href="https://ncatlab.org/nlab/revision/linearly+distributive+category/24">v24</a>, <a href="https://ncatlab.org/nlab/show/linearly+distributive+category">current</a>

    Added reference to linear bicategories

    Priyaa Srinivasan

    diff, v24, current

37. • CommentRowNumber37.
    • CommentAuthornLab edit announcer
    • CommentTime5 days ago
    • PermaLink
    Author: nLab edit announcer
    Format: MarkdownItexAdded reference to linear bicategories Priyaa Srinivasan <a href="https://ncatlab.org/nlab/revision/diff/linearly+distributive+category/24">diff</a>, <a href="https://ncatlab.org/nlab/revision/linearly+distributive+category/24">v24</a>, <a href="https://ncatlab.org/nlab/show/linearly+distributive+category">current</a>

    Added reference to linear bicategories

    Priyaa Srinivasan

    diff, v24, current