As described above, one of the motivations for CloTT is the encoding of coinductive types capturing
the notion of productivity in types. There exist other solutions to this problem, in particular the combination of
single clock guarded recursion with an `always' modality \(\Box \)  [1]}, [2]}
and sized types [3]}, [4]}, [5]}, [6]}. We refer to [7]}
for a discussion of the relationship between these approaches.
