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

[Nils Anders Danielsson]

On 2013-08-22 17:00, Jonathan Leivent wrote:
> Just to be clear, do you intend the "suc" only for hetero equality,
> not normal prop equality?

I don't propose that we should change the definition of propositional
equality.

-- 
/NAD