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

[Nils Anders Danielsson]

On 2009-12-11 20:29, Daniel Peebles wrote:
> As the new Pred you suggest introduces a new argument, would it not be
> better to go with the REL/Rel distinction and make a PRED/Pred pair,
> for backwards compatibility? Or is the REL/Rel pair just a stopgap
> measure?

REL/Rel will probably change before the next release of the library.

--
/NAD