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

[Jonathan Leivent]

On 08/19/2013 01:13 PM, Wolfram Kahl wrote:
> ...
> 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?

Can the question be broken into two parts - a practical and a 
theoretical part?  The practical part is: what safe but possibly 
restrictive general rule can be adopted (and put into the type checker 
as a default, maybe?) as an interim solution.  The least (or lesser) 
restrictive "appropriate general" rule would be the theoretical question.

-- Jonathan