subtype vs psigma

Stream: new members

[Sebastian Zimmer]

What is the difference between {a:α // p a} and Σ' a, P a?
It seems like they are both a dependent pair.

[Chris Hughes]

psigma is a less restrictive definition than subtype, because the second element does not have to be a proof, but for subtypes it does.

[Sebastian Zimmer]

So in the case where the second element is a proof, which one would you recommend using?

[Chris Hughes]

Definitely subtype. Subtypes have the extensionality rule, that two elements are equal iff the first of the pair is equal, which is very handy.