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

[Jonathan Leivent]

Propositional equality is defined in the standard library as:

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

Why isn't it just:

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

The same question applies to many other "proof term" types.

-- Jonathan Leivent