Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

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?

like image 370
Konstantin Solomatov Avatar asked Mar 30 '14 21:03

Konstantin Solomatov


1 Answers

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.

like image 78
Jesper Avatar answered Sep 30 '22 17:09

Jesper