nLab product extensionality



The counterpart to function extensionality but for products/pairs of elements (a,b)(a, b). Product extensionality characterizes the equality of elements in cartesian products in set theory and product types in type theory.


In set theory

Product extensionality states that for all elements aAa \in A, aAa' \in A, bBb \in B, and bBb' \in B, a=aa = a' and b=bb = b' if and only if (a,b)=(a,b)(a, b) = (a', b'). Product extensionality is sometimes assumed as an axiom in material set theory to make the pairing structure into an ordered pairing structure (a,b)(a, b).

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 AA and BB, the binary function application to identities apbinary (,)(a,a,b,b)\mathrm{apbinary}_{(-,-)}(a, a', b, b') of the function a:A,b:B(a,b):A×Ba:A, b:B \vdash (a, b):A \times B defined in the introduction rule for the product type is an equivalence of types for all elements a:Aa:A, a:Aa':A and b:Ab:A, b:Ab':A:

prodext(a,a,b,b):isEquiv(apbinary (,)(a,a,b,b))\mathrm{prodext}(a, a', b, b'):\mathrm{isEquiv}(\mathrm{apbinary}_{(-,-)}(a, a', b, b'))

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 AA and BB and elements a:Aa:A, a:Aa':A, b:Bb:B, and b:Bb':B,

(a,b)= A×B(a,b)(a= Aa)×(b= Bb)(a, b) =_{A \times B} (a', b') \equiv (a =_A a') \times (b =_B b')

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 𝟚\mathbb{2}. Indeed, given types AA and BB, we can define a type family CC indexed by 𝟚\mathbb{2} as C(0)AC(0) \coloneqq A and C(1)BC(1) \coloneqq B. Then A×BA \times B is the same as x:𝟚C(x)\prod_{x:\mathbb{2}} C(x).

We define c: x:𝟚C(x)c:\prod_{x:\mathbb{2}} C(x) and c: x:𝟚C(x)c':\prod_{x:\mathbb{2}} C(x) by c(0)ac(0) \coloneqq a, c(1)bc(1) \coloneqq b, c(0)ac'(0) \coloneqq a', c(1)bc'(1) \coloneqq b'.

There is a canonical function

idstodepprodid(c,c):(c(0)= C(0)c(0))×(c(1)= C(1)c(1))(c= x:𝟚C(x)c)\mathrm{idstodepprodid}(c, c'):(c(0) =_{C(0)} c'(0)) \times (c(1) =_{C(1)} c'(1)) \to (c =_{\prod_{x:\mathbb{2}} C(x)} c')

inductively defined by

idstodepprodid(c,c)(refl C(0)(c(0)),refl C(1)(c(1)))refl x:𝟚C(x)(c):Ω( x:𝟚C(x),c)\mathrm{idstodepprodid}(c, c)(\mathrm{refl}_{C(0)}(c(0)), \mathrm{refl}_{C(1)}(c(1))) \equiv \mathrm{refl}_{\prod_{x:\mathbb{2}} C(x)}(c):\Omega(\prod_{x:\mathbb{2}} C(x), c)

where Ω(A,a)\Omega(A, a) is the loop space type a= Aaa =_A a of AA at a:Aa:A.

We could also make (c(0)= C(0)c(0))×(c(1)= C(1)c(1))(c(0) =_{C(0)} c'(0)) \times (c(1) =_{C(1)} c'(1)) into a dependent product as well, as ( x:𝟚(c(x)= C(x)c(x)))\left(\prod_{x:\mathbb{2}} (c(x) =_{C(x)} c'(x))\right), making the above function

idstodepprodid(c,c):( x:𝟚(c(x)= C(x)c(x)))(c= x:𝟚C(x)c)\mathrm{idstodepprodid}(c, c'):\left(\prod_{x:\mathbb{2}} (c(x) =_{C(x)} c'(x))\right) \to (c =_{\prod_{x:\mathbb{2}} C(x)} c')

Product extensionality is the statement that the function idstodepprodid(c,c)\mathrm{idstodepprodid}(c, c') is an equivalence of types for all elements c: x:𝟚C(x)c:\prod_{x:\mathbb{2}} C(x) and c: x:𝟚C(x)c':\prod_{x:\mathbb{2}} C(x):

prodext(c,c):isEquiv(idstodepprodid(c,c))\mathrm{prodext}(c, c'):\mathrm{isEquiv}(\mathrm{idstodepprodid}(c, c'))

See also


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.