CODEWITHSUNDEEP
agdadependent-type
Konstantin Solomatov
Konstantin Solomatov

Reputation: 10332

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?

Upvotes: 6

Views: 442

Answers (1)

Jesper
Jesper

Reputation: 2945

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.

Upvotes: 6

Related Questions