[Agda] Size of propositional equality?

[Alan Jeffrey]

Hi all,

In v0.3 of the standard library, propositional equality is defined:

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

In v0.4 the definition has changed to:

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

That is, (x ≡ y) used to be a Set, now it is a (Set a) where a is the 
universe of x and y's type.  This change is breaking some code of mine 
(in a case where I'd jumped through some indexing hoops to make sure a 
type was a Set rather than a Set_1).

I'm sure there's a good reason for this change, any hints what it might be?

A.