[Agda] Prop was removed in 2.2.8

[Pavel Perikov]

On Aug 25, 2011, at 5:44 PM, Ulf Norell wrote:

> 
> It was an experimental universe whose inhabitants (if you enabled the flag --proof-irrelevance) were syntactically restricted to have at most one element. The idea was that you could get proof irrelevance for Prop cheaply. It didn't quite work out, so we removed it.

Thanks! So now the cost for the proof irrelevance was paid and there's need for Prop?

P.