The work presented here builds on a number of existing models for guarded recursion. The most basic such, modelling the
single clock case, is the topos of trees model [1]},
in which a closed type is modelled as a family of sets
\(X_n\)  indexed by natural numbers \(n\) , together with restriction maps of the form \(X_{n+1} \rightarrow X_n\)  for every \(n\) . In other
words, a type is a presheaf over the ordered natural numbers. In this model \(\triangleright \)  is modelled as \((\triangleright X)_0 = 1\)  and
\((\triangleright X)_{n+1} = X_n\)  and guarded recursion reduces to natural number recursion. The guarded recursive
type \(\mathsf {Str}^{\mathsf {g}}\)  mentioned above can be modelled in the topos of trees as
\(\mathsf {Str}^{\mathsf {g}}_n = \mathbb {N}^{n+1}\times 1\) .
