A well-founded order is a set $𝐷$ with a proposition-valued transitive relation $<$ admitting no infinite descent: every element is accessible. Write $𝑎\le 𝑏$ for $(𝑎<𝑏)\vee (𝑎=𝑏)$.

A direct structure on a category $\mathrm{𝒞︀}$ over $(𝐷,<)$ is a functor

into the well-founded order viewed as a poset category. The functor organizes two pieces of data at once: an ordering on the objects, and the invariant that morphisms respect it — $𝑓:𝑥\to 𝑦$ forces $\text{deg}𝑥\le \text{deg}𝑦$.

A direct structure equips the objects with a well-founded strict relation

Intuitively, direct categories are the right generalization of well-foundedness to the categorical setting: a direct category is essentially one whose underlying graph is a directed acyclic graph, layered by degree, so that data at an object may be defined by recursion from data at all objects strictly below it.

The degrees order the objects, while the morphisms of $\mathrm{𝒞︀}$ say how an object sits over its predecessors.

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.

Fix an endofunctor $𝐹:\mathrm{𝒞︀}\to \mathrm{𝒞︀}$. A coalgebra $𝛾:𝑋\to 𝐹𝑋$ is recursive when for every algebra $𝛼:𝐹𝐵\to 𝐵$ there is exactly one hylomorphism $ℎ:𝑋\to 𝐵$ from $𝛾$ to $𝛼$, that is, exactly one solution of

Equivalently, the functor $\text{𝖧𝗒𝗅𝗈}(𝛾,-)$ of the hylomorphism profunctor is constantly a singleton.

Recursiveness is a coalgebraic form of well-foundedness: $𝛾$ decomposes each input into subproblems, and recursiveness says that every divide-and-conquer program built on this decomposition has a unique meaning, without mentioning an order on inputs. [1] use recursive coalgebras on categories of indexed families to obtain algorithms that are correct by the type of the map they compute.

Example. If $(𝜇𝐹,\text{𝗂𝗇})$ is an initial algebra, then $\text{𝗂𝗇}$ is invertible (Lambek’s lemma) and ${\text{𝗂𝗇}}^{-1}:𝜇𝐹\to 𝐹(𝜇𝐹)$ is a recursive coalgebra. Precomposing with the isomorphism $\text{𝗂𝗇}$, the equation $ℎ={\text{𝗂𝗇}}^{-1}\star 𝐹ℎ\star 𝛼$ is equivalent to $\text{𝗂𝗇}\star ℎ=𝐹ℎ\star 𝛼$, which says $ℎ$ is an algebra map out of the initial algebra; there is exactly one, $\text{𝖿𝗈𝗅𝖽}𝛼$.

The dual notion is a corecursive algebra.