[Agda] Bin._<_

[Nils Anders Danielsson]

On 2012-08-04 11:15, Andreas Abel wrote:
> To get least possible levels, we could switch to cumulative universes.
> That would also greatly reduce the amount of levels since you can
> silently cast A : Set a to A : Set (lsuc a). It is on my todo list,
> but so are many other things, and the changes to the Agda core would
> be substantial.

How do you propose to introduce cumulativity? Conor writes the following
in "Crude but Effective Stratification":

   "You can leave levels implicit: there's a constraint-solver. The lack of
   cumulativity helps make constraint-solving tractable."

   http://www.e-pig.org/epilogue/?p=857

-- 
/NAD