## Stream: new members

### Topic: subtype vs psigma

#### Sebastian Zimmer (Oct 14 2018 at 18:07):

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

#### Chris Hughes (Oct 14 2018 at 18:08):

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 (Oct 14 2018 at 18:09):

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

#### Chris Hughes (Oct 14 2018 at 18:10):

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

Last updated: May 14 2021 at 04:22 UTC