The tensor of grammars,

is simply typed, so $𝐵$ cannot see what $𝐴$ matched.

Just as we have the generalization from the pair type $𝐴\times 𝐵$ to the dependent pair ${\mathrm{\Sigma }}_{𝑎:𝐴}𝐵𝑎$, we can define a dependent tensor operation. It is a $\mathrm{\Sigma }$-like generalization over the ordinary tensor, in which the second grammar depends on a parse tree of the first.

Write $\text{𝖳𝗋𝖾𝖾}(𝐴)={\sum }_{𝑤}𝐴(𝑤)$ for the type of parse trees of $𝐴$, each paired with the string it parses.

For a grammar $𝐴$ and a family of grammars $𝐵:\text{𝖳𝗋𝖾𝖾}(𝐴)\to \text{𝐆𝐫}$, the dependent tensor is:

We may also write it as $(𝑎\in 𝐴)\otimes 𝐵(𝑎)$.

When $𝐵$ is a constant family, the dependent tensor reduces to the ordinary tensor $𝐴\otimes 𝐵$.

Dependence runs left to right here, which fits left-to-right parsing. The other handedness, in which the first grammar depends on a parse of the second, is also definable.

Relation to Day Convolution

Just as the ordinary tensor is given by Day convolution, I think there is a similar dependent Day convolution for which this operation is an instance. My best guess is for any $𝑋$ presheaf on a monoidal category $\mathrm{𝒞︀}$ and $𝑌$ a functor from the category of elements of $𝑋$ into presheaves on $\mathrm{𝒞︀}$,

$\left(𝑋{\otimes }^{\text{𝖣}}𝑌\right)𝑐={\int }^{𝑢,𝑣}\mathrm{𝒞︀}[𝑐,𝑢\otimes 𝑣]\times {\int }^{𝑥:𝑋𝑢}𝑌(𝑢,𝑥)𝑣$

I’m not positive on this though, and I would hope to also extend this to enrichments that aren’t $\text{𝐒𝐞𝐭}$ but I don’t see how that could make sense given that I have quantified over the element $𝑥:𝑋𝑢$ in the coend rather than using the tensor of the enriching category.