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

[Wolfram Kahl]

On Mon, Aug 19, 2013 at 04:59:08PM +0100, Martin Escardo wrote:
> It would be good if somebody with experience in both intensional MLTT
> and HoTT wrote down explicitly what the correct universe levels of
> identity types are in the presence of a tower of universes indexed by
> natural numbers, for the record.

The next question then is:
How does this come out as a special case from an appropriate general
rule for parameterised and indexed inductive datatypes?

Because, as far as I know, that is what the definition of
propositional equality is for Agda, since Agda has no separate concept
of ``identity types'' in the language --- or am I mistaken here?


Wolfram