Zulip Chat Archive

Stream: new members

Topic: subtype vs psigma


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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