nLab weak function extensionality

Definition

The principle of weak function extensionality states that the dependent product type of a family of contractible types is itself contractible.

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B \; \mathrm{type} \quad \Gamma, x:A \vdash p(x):\mathrm{isContr}(B(x))}{\Gamma \vdash \mathrm{weakfunext}(\lambda x.p(x)):\mathrm{isContr}\left(\prod_{x:A} B(x)\right)}$$

This is equivalent to the condition that the dependent product type of a family of h-propositions itself is an h-proposition:

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B \; \mathrm{type} \quad \Gamma, x:A \vdash p(x):\mathrm{isProp}(B(x))}{\Gamma \vdash \mathrm{weakfunext}(\lambda x.p(x)):\mathrm{isProp}\left(\prod_{x:A} B(x)\right)}$$

Weak function extensionality is not equivalent to the principle of unique choice. The principle of unique choice states that the dependent product type of a family of contractible types is pointed

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B \; \mathrm{type} \quad \Gamma, x:A \vdash p(x):\mathrm{isContr}(B(x))}{\Gamma\vdash \mathrm{uniquechoice}(\lambda x.p(x)):\prod_{x:A} B(x)}$$

Properties

• Weak function extensionality is equivalent to function extensionality.

• In the presence of a universe of all propositions $\Omega$, weak function extensionality is equivalent to impredicative polymorphism for $\Omega$.

 See also

• function extensionality
• principle of unique choice

 References

Weak function extensionality appears in section 13.1 of

• Egbert Rijke, Introduction to Homotopy Type Theory, Cambridge Studies in Advanced Mathematics, Cambridge University Press (pdf) (478 pages)