Definition. Later on presheaves
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 precomposes with the induced map . 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.