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

[Ulf Norell]

On Sun, May 11, 2008 at 5:11 AM, Samuel Bronson <naesten at gmail.com> wrote:

> I seem to be in over my head. Help!
>

Here are the relevant bits:

record IsEquivalence {a : Set} (_≈_ : Rel a) : Set where ...
>
record Theory : Set1 where ...
>
record _≅_ (S : Theory) (T : Theory) : Set where ...
>
≅-isEquivalence : IsEquivalence _≅_
>

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...

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20080511/122be96d/attachment.html