Say your context is full of propositions at labels p that can be the identity, or a variable, or a (not necessarily commutative!) monoid operation or maybe some other function symbols:
I assume the monoid operation * is associative, and has unit e.
I'm going to need to lift the monoid operation to an action on contexts, but this is totally straightforward:
I then get two interesting modalities, one positive and one negative:
I seem to be forced into this ordering by considering the general case where * is not commutative. I kind of expected modalities to synchronously demand stuff be pulled off the same end that they put it on, but they don't --- they insert and delete at opposite ends of monoid expressions. Maybe this is another shadow of whatever phenomenon makes queue logic happen instead of stack logic?
Anyway I am pretty sure the circle operation I'd been talking about up until now is this box-plus, and the filled-circle I want is box-minus. The plain old conjunction and disjunction and units don't do anything interesting here; they just propagate (or allow) all labels. But implication takes just a little bit of care:
Although I'm writing contexts as Γ and Δ, I still understand contraction and weakening to be implicitly allowed. I just have to do a context merge in implies-left because one of the contexts gets hit with a [p *], while the other doesn't.
Here's what identity and cut:
And here's the encodings of tensor and its right adjoint that I think are correct for some value of "correct":
(full image here)
