# 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