[Agda] Level constraints

[Nils Anders Danielsson]

On 2013-11-14 23:05, Martin Escardo wrote:
> 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.

Harper and Pollack (1991) describe several algorithms. I assume that you
are referring to the one in Section 6.2 (with both typical ambiguity and
universe polymorphism). I seem to recall reading that one implementation
of this algorithm was very slow, but unfortunately I don't remember
where I read this. Is Matthieu's implementation of universe polymorphism
in Coq based on this algorithm?

-- 
/NAD