Author: nLab edit announcer Format: MarkdownItexThis is the extensionality principle for cartesian products in set theory and product types in type theory.
Anonymous
<a href="https://ncatlab.org/nlab/revision/product+extensionality/1">v1</a>, <a href="https://ncatlab.org/nlab/show/product+extensionality">current</a>
This is the extensionality principle for cartesian products in set theory and product types in type theory.
Author: nLab edit announcer Format: MarkdownItexadded a sentence stating that product extensionality is usually assumed as an axiom in set theory with ordered pairing structure.
Anonymous
<a href="https://ncatlab.org/nlab/revision/diff/product+extensionality/5">diff</a>, <a href="https://ncatlab.org/nlab/revision/product+extensionality/5">v5</a>, <a href="https://ncatlab.org/nlab/show/product+extensionality">current</a>
added a sentence stating that product extensionality is usually assumed as an axiom in set theory with ordered pairing structure.
Author: nLab edit announcer Format: MarkdownItexediting definition to make it valid for positive product types, where the projection functions $\pi_1$ and $\pi_2$ in the negative product types don't come with the elimination rules for the positive product types.
Anonymous
<a href="https://ncatlab.org/nlab/revision/diff/product+extensionality/6">diff</a>, <a href="https://ncatlab.org/nlab/revision/product+extensionality/6">v6</a>, <a href="https://ncatlab.org/nlab/show/product+extensionality">current</a>
editing definition to make it valid for positive product types, where the projection functions $\pi_1$ and $\pi_2$ in the negative product types donâ€™t come with the elimination rules for the positive product types.