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

[Jonathan Leivent]

On 08/18/2013 04:39 PM, Andreas Abel wrote:
> Putting propositional equality in a lower universe than the type it
> speaks about is at least problematic when you want to construct a PER
> model of type theory predicatively.

As a non-type-theorist trying to use Agda, I don't have the intuitions 
needed here to know I'm treading on uncertain ground.  So, I was relying 
on the type checker.  Is there some option I can use that will cause the 
type checker to enforce this rule?

-- Jonathan