[Agda] Universe Hierarchy Problem?

[Nils Anders Danielsson]

On 2009-12-07 03:42, kahl at cas.mcmaster.ca wrote:
> I have managed to get the error message (from Agda-2.2.4):
>
>   Set !=< Set1
>
> To me, that seems to indicate the claim that Set is not a subtype of
> Set1, [...]

Set is not a subtype of Set₁.

--
/NAD