Axiom of choice in type theory

Statement

In type theory, a different kind of statement is known as the axiom of choice. This form begins with two types, σ and τ, and a relation R between objects of type σ and objects of type τ. The axiom of choice states that if for each x of type σ there exists a y of type τ such that R(x,y), then there is a function f from objects of type σ to objects of type τ such that R(x,f(x)) holds for all x of type σ:

$$(\forall x^\sigma)(\exists y^\tau) R(x,y) \to (\exists f^{\sigma \to \tau})(\forall x^\sigma) R(x,f(x)).$$

Unlike in set theory, the axiom of choice in type theory is typically stated as an axiom scheme, in which R varies over all formulas or over all formulas of a particular logical form.