Write $𝑢⊏𝑣$ when $𝑢$ is a proper suffix of $𝑣$, that is, $𝑣=𝑥\text{++}𝑢$ with $𝑥\ne 𝜀$. The later of a grammar $𝐴$ is

A parse of $▷𝐴$ over $𝑣$ is a parse of $𝐴$ over every proper suffix of $𝑣$. In particular $(▷𝐴)𝜀$ is a singleton.

This is later on families for strings under the proper-suffix order. That order is well-founded because it strictly decreases length, so it is a thin direct category. There is at most one map $𝑢\to 𝑣$, so the product over maps from the strict past has one factor per proper suffix. Guarded recursion is modelled by presheaves on $𝜔$, the topos of trees, and more generally by sheaves over a well-founded base [1]. Here the later acts on families, which is what grammars are, and there is no clock.

Later is the right adjoint of the proper-suffix derivative. Let $\text{𝖭𝖤𝖲}={⨁}_{𝑥\ne 𝜀}\lceil 𝑥\rceil$ be the grammar of non-empty strings. Then the derivative $({𝜕}_{\text{𝖭𝖤𝖲}}𝐵)𝑢\cong {\sum }_{𝑥\ne 𝜀}𝐵(𝑥\text{++}𝑢)$ has the right adjoint

so ${𝜕}_{\text{𝖭𝖤𝖲}}-⊣▷$. Splitting $\text{𝖭𝖤𝖲}$ into its summands gives the form of $▷$ that the calculus can define:

The component at $𝑤$ says: if the string begins with $𝑤$, then the rest parses as $𝐴$.

The restriction to non-empty $𝑤$ is what makes this a later. At $𝑤=𝜀$ the component is $\sqrt[\lceil 𝜀\rceil ]{𝐴}\cong 𝐴$. Including it would give a projection $▷𝐴⊢𝐴$, and Löb would then prove every grammar. For the same reason the later is a product over suffixes. A sum such as ${⨁}_{𝑐}\lceil 𝑐\rceil ⊸𝐴$ is empty at $𝜀$, and at $𝐴=\perp$ it is $\perp$. The identity step $\perp ⊢\perp$ would then give Löb a proof of $\top ⊢\perp$.

In the Agda this is ▷ in Grammar/Later/Base.agda, which is defined as the indexed conjunction of √l-string. The mirror image ▷r, over proper prefixes, is defined in the same way. See also the bilateral later and the later along an arbitrary well-founded order.