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

[Wolfram Kahl]

On Sat, Aug 17, 2013 at 04:52:02PM -0400, Jonathan Leivent wrote:
> 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.

I have a module |Relation.Binary.PropositionalEquality.Generalised| containing:

----------------------------------------------------------------------------
We define a fully |Level|-polymorphic variant of propositional equality
in order to be able to define fully |Level|-polymorphic identity relations.
(Thorsten Altenkirch%
\footnote{at AIM XIII, April 2011}
 and others
 have expressed reservations whether such a definition
 at levels |k| lower than |a| should be legal.)

\begin{code}
  data _≡≡_  {k a : Level} {A : Set a} (x : A) : A → Set k where
    ≡≡-refl : x ≡≡ x
\end{code} 
----------------------------------------------------------------------------

Because of those comments, I use it only in isolated contexts,
because one day somebody might come along and prove that I am using an
unsafe feature of Agda, which might then get removed...


Wolfram