How to use Prop from UTT in Agda In Ulf Norell's thesis he mentions that Agda is based on Luo's UTT. However, I can't find a way to use Prop there. Is there any way to do so?
In Agda this is done by tagging types as "irrelevant". It's a kind of quotenting. A function from an irrelevant to a (relevant) type must be constant (and Agda enforces this). You can read more about it on the Agda wiki Irrelevance page.