# Start a new discussion

## Not signed in

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

## Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorDavid_Corfield
• CommentTimeJun 20th 2018

At our workshop yesterday we heard Dominic Orchard speak about “Graded Modal Logic for Linear Dependent Type Theory”/ So I’ve started graded modality.

Now any connection to Licata-Shulman-Riley?

• CommentRowNumber2.
• CommentAuthorDavid_Corfield
• CommentTimeJun 20th 2018

It would seem so, seeing that LSR speaks about subexponentials in 3.10.

How about the $\sharp_n$ of section 5.2.2 of dcct, or the $\Im_n$ mentioned e.g. here? Are these not modalities indexed by the natural numbers with monoid operation given by min? Similarly for truncation modalities.

• CommentRowNumber3.
• CommentAuthorUrs
• CommentTimeJun 20th 2018

• CommentRowNumber4.
• CommentAuthorMike Shulman
• CommentTimeJun 20th 2018

I haven’t looked at any of the references, but almost without exception anything like this has a representation using a particular mode theory in LSR; here there would presumably be an infinite family of mode morphisms with 2-cells between them representing the rule structure.

• CommentRowNumber5.
• CommentAuthorDavid_Corfield
• CommentTimeJun 26th 2018

• CommentRowNumber6.
• CommentAuthorDavid_Corfield
• CommentTimeDec 18th 2018

• CommentRowNumber9.
• CommentAuthorDavid_Corfield
• CommentTimeJun 25th 2021

• CommentRowNumber10.
• CommentAuthorJ-B Vienney
• CommentTimeAug 5th 2022
• (edited Aug 5th 2022)

• Flavien Breuvart, Michele Pagani, Modelling Coeffects in the Relational Semantics of Linear Logic, (pdf)
• CommentRowNumber11.
• CommentAuthorJ-B Vienney
• CommentTimeAug 25th 2022
• (edited Aug 25th 2022)

Recent variations of linear logic using graded modalities could be named by the expression “graded linear logic”. Bounded linear logic is something quite specific.

I will create these pages later.

• CommentRowNumber12.
• CommentAuthorJ-B Vienney
• CommentTimeAug 25th 2022
• (edited Aug 25th 2022)

Added that the homological linear logic would be linked with Koszul complexes.

• CommentRowNumber13.
• CommentAuthorJ-B Vienney
• CommentTimeAug 25th 2022
• (edited Aug 25th 2022)

Added also a link to symmetric linear logic which is meant to be a logic of symmetric powers or equivalently a logic of homogeneous polynomials and would be able to differentiate them by respecting the Euler identity.

• CommentRowNumber14.
• CommentAuthorJ-B Vienney
• CommentTime2 days ago

Added our preprint Graded Differential Categories and Graded Differential Linear Logic with JS Lemay in the references

3. Re #14, one of these days, someone’s going to need to work out whether and how this differential linear logic approach relates to the linear differential cohesive approach. I tried to get a conversation going on this over here and Tim Campion provided some useful comparison.

• CommentRowNumber16.
• CommentAuthorJ-B Vienney
• CommentTime2 days ago
• (edited 2 days ago)

The linear differential cohesive approach is far above my head. But if you have some linear HoTT framework (or something else) where there is an exponential modality, then we can maybe try to make this a differential exponential modality which will give a differential linear HoTT (resp. a differential something else).

4. The exponential modality is discussed here.

• CommentRowNumber18.
• CommentAuthorJ-B Vienney
• CommentTime2 days ago
• (edited 2 days ago)

Is $\Sigma_{+}^\infty \circ \Omega^\infty$ a monad or a comonad? Models of linear logic are traditionally with a comonad but in math, you more often have a monad (but then you can still obtain a model of “co”linear logic by reversing all the morphisms in the definition).

If you want differentiation, you need mainly your $\Sigma_{+}^\infty(\Omega^\infty(A))$ to be bialgebras.

5. Right adjoint first, so a comonad. I was managing to mix myself up over here, where I was speculating on there being a relevant graded version of the exponential.

• Please log in or leave your comment as a "guest post". If commenting as a "guest", please include your name in the message as a courtesy. Note: only certain categories allow guest posts.
• To produce a hyperlink to an nLab entry, simply put double square brackets around its name, e.g. [[category]]. To use (La)TeX mathematics in your post, make sure Markdown+Itex is selected below and put your mathematics between dollar signs as usual. Only a subset of the usual TeX math commands are accepted: see here for a list.

• (Help)