For presheaves, $\text{𝗇𝖾𝗑𝗍}:𝑃\to ▷𝑃$ restricts along the strict past, as in later on presheaves. A grammar is only a family over strings, so a map $\text{𝗇𝖾𝗑𝗍}:𝐴⊢▷𝐴$ into the later on grammars is extra data. It sends a parse over $𝑣$ to parses over every proper suffix of $𝑣$.

Let $\square 𝐴=𝐴\&▷𝐴$, so that $(\square 𝐴)𝑣\cong {\prod }_{𝑢⊑𝑣}𝐴𝑢$. This is the comonad $𝑈\circ \text{Cofree}$ for the suffix order, and presheaves are comonadic over families. The counit law forces the first component of a coalgebra $𝐴⊢\square 𝐴$ to be the identity. Hence:

• a presheaf on strings under the suffix order is the same as a grammar $𝐴$ with a map $\text{𝗇𝖾𝗑𝗍}:𝐴⊢▷𝐴$ that satisfies coassociativity. Restricting to $𝑢\prime$ and then to $𝑢⊏𝑢\prime$ must agree with restricting to $𝑢$ directly;
• for a proposition-valued grammar (a language), coassociativity is automatic, and $\text{𝗇𝖾𝗑𝗍}$ exists exactly when the language is closed under suffixes. For example, $\top$ has one, but $\lceil 𝑎\rceil$ does not, since $(▷\lceil 𝑎\rceil )𝑎\cong \lceil 𝑎\rceil 𝜀$ is empty.

Löb does not need $\text{𝗇𝖾𝗑𝗍}$ on $𝐴$. The fixed-point equation only restricts a global parse $\top ⊢𝐴$, and a global parse can always be restricted. In the Agda, the grammar-level IsCoalgebra record, with only the field next, is in Grammar/Later/Coalgebra.agda on the guarded branch.

On presheaves the strict downset of $𝑐\text{++}𝑡$ is represented by $𝑡$, because every proper suffix of $𝑐\text{++}𝑡$ is a suffix of $𝑡$. So predecessors simplify later to $(▷𝑃)(𝑐\text{++}𝑡)\cong 𝑃𝑡$. On grammars there is no such simplification, since the factors at different suffixes are unrelated.