Later takes a limit over smaller indices. Dually, the earlier modality takes a colimit over larger indices: an element of $⊲𝑃$ at $𝑥$ is a $𝑃$-element sitting at some object $𝑦$ strictly above $𝑥$, carried down along a chosen morphism $𝑥\to 𝑦$.

Earlier is left adjoint to later:

Under this adjunction, $\text{𝗇𝖾𝗑𝗍}:𝑃\to ⊳𝑃$ corresponds to

.

Conjugation with the adjunction between presheaves and families $𝑈⊣\text{Cofree}$ lets us induce a later construction on families from the one on presheaves,

Concretely, later on families evaluates to

The later modality for presheaves on a direct category is given by the presheaf of natural transformations

out of the strict downset.

An element of $⊳𝑃$ at $𝑥$ is a coherent choice of $𝑃$-elements at all objects strictly smaller than $𝑥$.

Restriction in $⊳𝑃$ along $𝑓:𝑦\to 𝑥$ precomposes with the induced map $\text{𝖲𝗍𝗋𝗂𝖼𝗍𝖣𝗈𝗐𝗇}(𝑦)\to \text{𝖲𝗍𝗋𝗂𝖼𝗍𝖣𝗈𝗐𝗇}(𝑥)$. At an object of minimal degree the strict downset is empty, so $⊳𝑃$ is trivial there.

Via functoriality, every presheaf restricts to smaller indices. Thus we may define the map

that sends an element $𝑝$ over $𝑥$ to the family of all its restrictions along morphisms from strictly lower objects.

Like later on families, the recursion principle for families is inherited from that on presheaves. Given a family $𝐴$ and a step

the construction is a chain of transpositions with Löb for presheaves used in the middle:

Just as for presheaves, the fixed point constructed above is unique: the two transpositions are bijections, and the presheaf-level fixed point is already unique.

Let $\mathrm{𝒞︀}$ be a direct category and $𝑃$ a presheaf on it. Every map

has a fixed point: a global element $\text{𝗅ö𝖻}𝜑:\top \to 𝑃$ with

and this fixed point is unique.

The hypothesis says: the value of $𝑃$ at any object is determined by its values over the strict past — $𝜑$ turns a coherent family over the strict downset of $𝑥$ into a value at $𝑥$. The proof is recursion along the well-founded $\prec$: at each $𝑥$, the section already constructed over the past assembles into an element of $(⊳𝑃)(𝑥)$, and $𝜑$ extends it to $𝑥$.

Write $𝑋\Rightarrow 𝑌$ for the presheaf of morphisms $𝑋\to 𝑌$. An endofunctor $𝐹$ on presheaves is locally contractive when its action on morphisms factors through later: there is a map

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.

For every grammar $𝐴$ and every term $𝜑:▷𝐴⊢𝐴$, where $▷$ is the later on grammars, there is a unique global parse $\text{𝗅ö𝖻}𝜑:\top ⊢𝐴$ with

Here $\text{𝗇𝖾𝗑𝗍}𝑡:\top ⊢▷𝐴$ restricts a global parse $𝑡$ to every proper suffix.

The proof is recursion on the length of the string. At $𝑣$, the parses already built at the proper suffixes of $𝑣$ form an element of $(▷𝐴)𝑣$, and $𝜑$ turns it into a parse at $𝑣$. Uniqueness is Löb for families over the proper-suffix order. In the Agda, lob in Grammar/Later/Base.agda is this recursion, done by well-founded induction on length.

To prove an entailment $𝐵⊢𝐶$ this way, apply Löb to $𝐴=𝐵\Rightarrow 𝐶$. The hypothesis $▷(𝐵\Rightarrow 𝐶)$ is the induction hypothesis at every proper suffix. It becomes usable once a non-nullable grammar has been consumed. If $𝜀\&𝐵⊢\perp$, then

because a parse of $𝐵\otimes \top$ over $𝑣$ splits $𝑣=𝑥\text{++}𝑢$ with $𝑥$ non-empty, so $𝑢⊏𝑣$. This is ▷-app-NE in Grammar/Later/Properties.agda. Induction on a Kleene star is the standard use.

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.