A predecessor of $𝑥$ is a top element of its strict downset: a strict morphism $𝜌:𝑝\to 𝑥$ through which every strict morphism into $𝑥$ factors uniquely. Equivalently, $\text{𝖲𝗍𝗋𝗂𝖼𝗍𝖣𝗈𝗐𝗇}(𝑥)\cong \text{𝗒}𝑝$ — the downset is representable.

The Yoneda lemma then collapses later to evaluation:

with $\text{𝗇𝖾𝗑𝗍}$ becoming restriction along $𝜌$. The name is from the naturals: every strict map into $𝑛+1$ factors through $𝑛\to 𝑛+1$, so on $𝜔$ — in the topos of trees — later is just the shift

and a Löb step is a base value together with a rule producing the value at $𝑛+1$ from the value at $𝑛$.

When this predecessor exists, we can give a simpler description of later, as in the topos of trees, but this may not be possible in all direct categories.