[Agda] Level constraints

[Nils Anders Danielsson]

On 2013-11-14 16:34, Christian Sattler wrote:
> What do you think?

There are many options (at least if we restrict the discussion to
lifting):

* The status quo.

* Something like what you suggest.

* Some kind of cumulativity.

* Conor's lifting primitive (Crude but Effective Stratification,
   http://sneezy.cs.nott.ac.uk/epilogue/?p=857.html).

* Allowing the solver to produce non-unique solutions. (I believe that
   Mattieu has implemented something like this for Coq.)

* …

I think it would be interesting to see a careful discussion of the pros
and cons of these different designs.

-- 
/NAD