Tag. right-adjoint

Notes (2)

Definition. Later on families later-family

Conjugation with the adjunction between presheaves and families π‘ˆβŠ£Cofree lets us induce a later construction on families from the one on presheaves,

⊳Fam=π‘ˆβˆ˜βŠ³βˆ˜Cofree:Fam(π’žοΈ€)β†’Fam(π’žοΈ€).

Concretely, later on families evaluates to

⊳Fam𝐴(π‘₯)β‰…βˆπ‘¦β‰Ίπ‘₯Β βˆπ‘“:𝑦→π‘₯𝐴(𝑦)

Definition. Later on presheaves later-presheaf

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.

tag-right-adjoint tag