Not signed in (Sign In)

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

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory history homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie lie-theory limit limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

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

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).

nLab > Latest Changes: graded modality

Bottom of Page

1 to 19 of 19

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

    v1, current

    • CommentRowNumber2.
    • CommentAuthorDavid_Corfield
    • CommentTimeJun 20th 2018

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

    How about the ♯ n\sharp_n of section 5.2.2 of dcct, or the ℑ n\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

    added hyperlink to modality, added hyperlink for bounded linear logic, added plural redirect

    diff, v3, current

    • 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

    Added a couple of references.

    diff, v4, current

    • CommentRowNumber6.
    • CommentAuthorDavid_Corfield
    • CommentTimeDec 18th 2018

    Added some earlier philosophical references.

    diff, v6, current

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

    Harley Eades III

    diff, v7, current

  8. A few more references, and added links to PDFs.

    Harley Eades III

    diff, v7, current

    • CommentRowNumber9.
    • CommentAuthorDavid_Corfield
    • CommentTimeJun 25th 2021

    Added some references

    diff, v15, current

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

    Added the reference

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

    diff, v16, current

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

    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.

    diff, v17, current

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

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

    diff, v17, current

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

    I will create this page later.

    diff, v17, current

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

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

    diff, v20, current

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

  17. 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 Σ + ∞(Ω ∞(A))\Sigma_{+}^\infty(\Omega^\infty(A)) to be bialgebras.

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

1 to 19 of 19

  1.  
Add your comments
  • 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)
 
Back to Discussions Top of Page