[Agda] Level constraints

[Martin Escardo]

On 14/11/13 22:02, Nils Anders Danielsson wrote:
> 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.

I thought I argued in the previous message that typical ambiguity, 
considered as a layer on top of what we have, precisely addresses the 
first three points. I have no idea about the last.

Best,
Martin