Contents
Idea
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.
Definition
In set 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 type theory
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 , :
Rules for product extensionality
Formation rules for the identity type of negative product types:
Introduction rules for the identity type of negative product types:
Elimination rules for the identity type of negative product types:
Computation rules for the identity type of negative product types:
Uniqueness rules for the identity type of negative product types:
These rules ensure that is a judgmental equivalence of types.
Judgmental product extensionality
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.
Relation to dependent product extensionality
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 :
See also
References
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: