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

[Nils Anders Danielsson]

On 2013-08-21 22:29, Jonathan Leivent wrote:
> 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.

Heterogeneous equality isn't very useful when --without-K is used.
Furthermore it's not quite clear to me how the definition should be
changed. The following, less universe-polymorphic definition seems
reasonable to me:

   data _≅_ {ℓ} {A : Set ℓ} (x : A) : {B : Set ℓ} → B → Set (suc ℓ) where
      refl : x ≅ x

If others agree, then I can switch to this definition.

-- 
/NAD