Hard to reply to such questions.

Best to just go ahead and add whatever material you feel like adding.

Once we see it, if we feel it would better fit into another entry, it’s easy to move it.

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

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

]]>The exponential modality is discussed here.

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

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

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

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.

I will create this page later.

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

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

Added a link to a new page graded linear logic.

Added a link to a new page graded differential linear logic.

Added a link to a new page homological linear logic.

I will create these pages later.

]]>Added the reference

- Flavien Breuvart, Michele Pagani,
*Modelling Coeffects in the Relational Semantics of Linear Logic*, (pdf)

Added some references

]]>A few more references, and added links to PDFs.

Harley Eades III

]]>Added a new reference to Fuji et al.’s paper on graded monads.

Harley Eades III

]]>Added some earlier philosophical references.

]]>Added a couple of references.

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

]]>added hyperlink to *modality*, added hyperlink for *bounded linear logic*, added plural redirect

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.

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

]]>