[Agda] Converting Relation.Unary to be universe-polymorphic

[Nils Anders Danielsson]

On 2009-12-11 16:34, Luke Palmer wrote:
> God forbid we should use multiple letters!
>
> (A : Set ℓa)
>
> Which doesn't interfere with the existing convention:
>
> (a : A) -> ...

This convention is rarely used in the library. If there is a conflict
between conventions, do whatever seems reasonable. I want to minimise
the noise created by universe levels, though.

--
/NAD