Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
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?
added hyperlink to modality, added hyperlink for bounded linear logic, added plural redirect
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.
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 that the homological linear logic would be linked with Koszul complexes.
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.
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.
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).
The exponential modality is discussed here.
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.
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.
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.
1 to 21 of 21