[Agda] Universe Hierarchy Problem?

[kahl at cas.mcmaster.ca]

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,
which surprises me --- according to Ulf's thesis,
UTT_{\Sigma} has  $Set = Set_0 \leq Set_1$,
and I could not find anything that indicates that Agda2
might differ from UTT_{\Sigma} on this count.

In the meantime, I have been able to work around it,
but nevertheless I am curious what the story is,
and where I should look for the current definition
--- is it really only in the Agda2 source code?


(I also managed to get  ``Set1 !=< Set'',
 and interpreted that as saying that Set1 is not a subtype of Set,
 which I understand, so I considered that message helpful!
)


Wolfram