The counterpart to function extensionality but for products/pairs of elements . Product extensionality characterizes the equality of elements in cartesian products in set theory and product types in type theory.
Product extensionality states that for all elements , , , and , and if and only if . Product extensionality is sometimes assumed as an axiom in material set theory to make the pairing structure into an ordered pairing structure .
In intensional type theory, equality is represented by the identity type, and furthermore, there might be more than one element of the identity type in intensional type theory, so a naive translation of product extensionality into intensional type theory doesn’t result in the right statement.
Instead, product extensionality is the statement that given types and , the binary function application to identities of the function defined in the introduction rule for the product type is an equivalence of types for all elements , and , :
One could replace the equivalence of types above with a judgmental equality of types, resulting in judgmental product extensionality, that for all types and and elements , , , and ,
Judgmental product extensionality holds in cubical type theory and higher observational type theory.
Product extensionality is equivalent to dependent product extensionality for dependent products indexed by the two-valued type . Indeed, given types and , we can define a type family indexed by as and . Then is the same as .
We define and by , , , .
There is a canonical function
inductively defined by
where is the loop space type of at .
We could also make into a dependent product as well, as , making the above function
Product extensionality is the statement that the function is an equivalence of types for all elements and :
For judgmental product extensionality in higher observational type theory, see
For a proof that the given function above between identity types is a quasi-inverse function in intensional type theory, see section 2.6:
Last revised on January 19, 2023 at 16:08:21. See the history of this page for a list of all contributions to it.