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.

later-presheaf definition entries/category/later-presheaf.hel