[Agda] Level ω

[David Leduc]

Hi,

I have a stream of levels (l0, l1, l2, l3 ...), and I want to define
what it is to be a stream of Sets li (for each i).
I tried the following definition.

  data T : Stream Level -> Set {!!} where
    makeT : (ls : Stream Level) -> Set (head ls) -> T (tail ls)

But to fill the hole, it seems I would need the level ω that is not available.
Is there a workaround?

To allow such definition, maybe Level should be defined coinductively like this:

  data Level : Set where
    zero : Level
    suc  : ∞ Level → Level

  ω : Level
  ω = suc (♯ ω)