[Agda] Someone please explain where Set1 comes into this...

[Samuel Bronson]

On Sun, May 11, 2008 at 6:21 AM, Ulf Norell <ulfn at cs.chalmers.se> wrote:

> IsEquivalence expects a relation over some Set a, but _≅_ is a relation over
> Theories which live in Set1. The error message could be a bit more
> detailed...

Yeah, just mentioning a few more levels of nesting in the attempted
unification would probably have helped...