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 and in the negative product types don’t come with the elimination rules for the positive product types.