Universal quantification over clocks allows for coinductive types to be encoded using guarded recursive types [1]}.
For example
\(\mathsf {Str}\mathbin {\overset{\textsf {def}}{=}}\forall \kappa . \mathsf {Str}^{\kappa }\)  is a coinductive type of streams. The head and tail maps \(\mathsf {hd} : \mathsf {Str}\rightarrow \mathbb {N}\)  and
\(\mathsf {tl} : \mathsf {Str}\rightarrow \mathsf {Str}\)  can be defined as
\(\mathsf {hd}(xs) & \mathbin {\overset{\textsf {def}}{=}}\pi _1(xs[\kappa _0]) &\mathsf {tl}(xs) & \mathbin {\overset{\textsf {def}}{=}}\Lambda \kappa . ((\pi _2(xs[\kappa ]))\,[\diamond ] )\) 
