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

[Jonathan Leivent]

On 08/22/2013 07:44 AM, Nils Anders Danielsson wrote:
> 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.
>

Just to be clear, do you intend the "suc" only for hetero equality, not 
normal prop equality?  So, normal prop equality would stay at its 
current level (Set ℓ), but hetero equality would be one level above?

-- Jonathan