[Agda] Level constraints

[Martin Escardo]

On 15/11/13 19:02, Wolfram Kahl wrote:
> Some of this can of course already be had by just writing ``Set _'',
> as it occurs quite frequently in the standard library.
> (I must admit that I do it rarely --- although I do have a definition
>   that takes over 30 (implicit) Level parameters.)
>
> Making the underlying metavariable instantiation even more intelligent
> would expand the opportunities for writing ``Set _''
> without any change to the language ---
> perhaps that could be one avenue for experimentation...

Nice, I will try to exploit this idea while typical ambiguity is not 
available (I am sure we will manage to persuade the great and kind Agda 
developers to eventually implement it). But I think the limitation of 
your solution could be when it comes to situations where i \sqcup j is 
needed for levels i and j, which is often the case (but perhaps I am 
wrong - I'd have to try).

Are you suggesting to define something like

Type {i} = Set i

(if that's possible) and then rely on implicit parameter inference to 
simulate (some of) typical ambiguity?

Best,
Martin