[Agda] Level ω

[Dan Doel]

On Sunday 26 September 2010 12:37:23 am David Leduc wrote:

> 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?

Not currently, at least.

> To allow such definition, maybe Level should be defined coinductively like
> this:
> 
>   data Level : Set where
>     zero : Level
>     suc  : ∞ Level → Level
> 
>   ω : Level
>   ω = suc (♯ ω)

This is not a solution, because then ω could appear in your stream, meaning 
that T would need to have type Set(ω+1).

There is, in fact, a Setω in Agda. But, you are not allowed to refer to it, 
nor does it have a type itself (so, trying to write a lambda expression that 
returns a universe polymorphic type will blow up; it is the top of the 
hierarchy). It is the type of universe polymorphic function spaces:

  ((i : Level) -> Set i) : Setω

I don't see anything wrong with allowing (co)inductive types to inhabit it as 
well, but it isn't even a reserved word, as I recall.

-- Dan