How to use Prop from UTT in Agda

Question

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?

Answer 1

The Prop universe was available in an early version of Agda, but it has since been removed. In fact, Prop is still a keyword in Agda, but using it gives an error Prop is no longer supported. Depending on what you want to achieve, you have a few options:

• You may want to take a look at Agda's proof irrelevance feature.

• I have seen some people use the synonym Prop = Set. This is useful if you want to make a logical difference between propositions and more general sets, but of course it doesn't give you any of the additional axioms of Prop.

• Finally, there is the type of (homotopy) propositions from HoTT, which can be defined in Agda by hProp = Σ[ X ∈ Set ] ((x y : X) → x ≡ y). This guarantees that propositions have at most one proof, but can cause quite some overhead.