This paper is part of a project to extend type theory with guarded recursion [1]}, a variant of
recursion that uses a modal type operator \(\triangleright \)  (pronounced `later')
to preserve consistency of the logical reading of type theory.
The type \(\triangleright A\)  should be read as classifying data of type \(A\)  available one time step from now, and comes with
a map \(\mathsf {next}: A \rightarrow \triangleright A\)  and a fixed point operator mapping a function \(f : \triangleright A \rightarrow A\)  to a fixed point for
\(f \circ \mathsf {next}\) . This, in combination with guarded recursive types, i.e., types where the recursion variable
is guarded by a \(\triangleright \) , e.g., \(\mathsf {Str}^{\mathsf {g}} \equiv \mathbb {N}\times \triangleright \mathsf {Str}^{\mathsf {g}}\)  gives a powerful type theory in which
operational models of combinations of advanced programming language features such as higher-order
store [2]} and nondeterminism [3]} can be modelled
using an abstract form of step-indexing [4]}.
Combining guarded recursion with a notion of clocks, indexing the \(\triangleright \)  operator with
clock names, and universal quantification over clocks, one can encode coinduction using guarded recursion,
allowing productivity [5]} of coinductive definitions to be encoded in types [6]}.
For example, if \(\mathsf {Str}^{\kappa }\)  is a type of streams guarded on the clock \(\kappa \) , i.e., satisfying the equation
\(\mathsf {Str}^{\kappa } \equiv \mathbb {N}\times \triangleright ^\kappa \mathsf {Str}^{\kappa }\) , then the type \(\mathsf {Str}\mathbin {\overset{\textsf {def}}{=}}\forall \kappa . \mathsf {Str}^{\kappa }\) 
obtained by universally
quantifying the clock \(\kappa \)  is a coinductive type of streams satisfying the more standard type isomorphism
\(\mathsf {Str}\cong \mathbb {N}\times \mathsf {Str}\) .
