Tag. right-adjoint
Notes (2)
Definition. Later on families later-family
Conjugation with the adjunction between presheaves and families lets us induce a later construction on families from the one on presheaves,
Concretely, later on families evaluates to
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.