Tag. left-adjoint
Notes (1)
Definition. Earlier on presheaves earlier-presheaf
Later takes a limit over smaller indices. Dually, the earlier modality takes a colimit over larger indices: an element of at is a -element sitting at some object strictly above , carried down along a chosen morphism .
Earlier is left adjoint to later:
Under this adjunction, corresponds to
.