[Agda] Why is propositional equality "Set a" instead of just Set?

[Jonathan Leivent]

Hetero equality is at level zero (in standard library 0.7):

-- Heterogeneous equality

infix 4 _≅_

data _≅_ {a} {A : Set a} (x : A) : ∀ {b} {B : Set b} → B → Set where
   refl : x ≅ x

I guess this can't be correct - or, at least, isn't consistent with 
where type theory is headed these days.

-- Jonathan