[Agda] [newbie] universe levels and BUILTIN EQUALITY

[Martin Stone Davis]

It's possible to define a kind of EQUALITY sorted in any universe we 
want. For example, Set₀:

data _≡_ {a} {A : Set a} (x : A) : A → Set₀
  where refl : x ≡ x

However, to be declarable as BUILTIN, the sort needs to be Set a. Why is 
it that way? It seems, to my naive eye, that it would be somehow simpler 
or more conservative to have it at the lowest level possible. What bad 
things would happen if it were required to be Set₀?