# [Agda] Level constraints

Martin Escardo m.escardo at cs.bham.ac.uk
Fri Nov 15 22:32:45 CET 2013

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

```