# [Agda] Level constraints

Wolfram Kahl kahl at cas.mcmaster.ca
Fri Nov 15 20:02:04 CET 2013

```On Thu, Nov 14, 2013 at 07:53:29PM +0000, Martin Escardo wrote:
> There is one more option, which I favour: Feferman's "typical
> ambiguity", with Harper's algorithm or similar.
>
> The idea is that you just write "Set", perhaps many times in the same
> definition, and then Agda adds (different) indices as appropriate. This
> feels like working with type-in-type, but it is actually working with
> what we already have, with the difference that the universe levels are
> inferred rather than written down.
>
> Moreover, it should be possible to be compatible with what we already
> have (perhaps writing e.g. Set_0 rather than Set if that's what you
> really mean). So, if you put levels i,j,k in your context and write
> Set_i, Set_{i \sqcup j}, etc. then it would work as it does now, but if
> you write Set in several places in the same definition, then it would
> invoke the typical ambiguity conventions and algorithm to fill in the
> missing indices and the missing indices. This should make things much
> easier, very much in the spirit of implicit arguments.

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

Wolfram
```