[Agda] Level constraints

[Nils Anders Danielsson]

On 2013-11-14 20:53, Martin Escardo wrote:
> There is one more option, which I favour: Feferman's "typical
> ambiguity", with Harper's algorithm or similar.

Harper and Pollack's algorithm? I omitted this algorithm, and other
methods that can be used to avoid writing things (like Twelf-style type
reconstruction for undeclared variables), because AFAICT they are (at
least partly) orthogonal to the issue raised in this thread.

My personal preference is (currently) to use something that satisfies
(at least) the following criteria:

* In "simple" cases I don't want to mention universe levels at all.

* In more complicated cases it should be possible to express exactly
   what I mean.

* The system shouldn't make decisions for me.

* The implementation should be efficient.

-- 
/NAD