We will assume given a countably infinite set \(\mathrm {CV}\)  of (semantic) clock variables, for which we use \(\lambda , \lambda ^{\prime },\dots \)  to range over.
A time object is a pair \((\mathcal {E};\delta )\)  where \(\mathcal {E}\)  is a finite subset of \(\mathrm {CV}\)  and
\(\delta :\mathcal {E}\rightarrow \mathbb {N}\)  is a map giving the number of ticks left on each clock in \(\mathcal {E}\) . We will write the finite sets
\(\mathcal {E}\)  as lists writing e.g., \(\mathcal {E}, \lambda \)  for \(\mathcal {E}\cup \lbrace \lambda \rbrace \)  and \(\delta [\lambda \mapsto n]\)  for the extension
of \(\delta \)  to \(\mathcal {E},\lambda \) , or indeed for the update of \(\delta \) , if \(\delta \)  is already defined on \(\lambda \) .
The time objects form a category \(\mathbb {T}\)  whose morphisms \((\mathcal {E};\delta )\rightarrow (\mathcal {E}^{\prime };\delta ^{\prime })\)  are functions
\(\tau :\mathcal {E}\rightarrow \mathcal {E}^{\prime }\)  such that
\(\delta ^{\prime }\tau \le \delta \)  in the pointwise order. The inequality allows for time to pass in a morphism, but morphisms can
also synchronise clocks in \(\mathcal {E}\)  by mapping them to the same clock in \(\mathcal {E}^{\prime }\) , or introduce new clocks if \(\tau \)  is not
surjective. Define \(\mathsf {GR}\)  to be the category \(\mathsf {Set}^{\mathbb {T}}\)  of covariant presheaves
on \(\mathbb {T}\) . The topos of trees [1]}
can be seen as a restriction of this where time objects always have a single clock.
