 Now, if this is to hold under a constructive interpretation, then for a given \(x \in A\), the value \(f(x)\) of the choice function will depend not only on \(x\) but also on the data proving that \(x\) belongs to \(A.\) In general, we cannot expect to produce a choice function of this sort. However, the BHK interpretation of the hypotheses in the axiom is that there is an algorithm \(\mathcal{A}\) which, applied to any given \(x \in A\), produces an element \(y \in B\) such that \((x,y) \in S\). If \(A\) is a completely presented set, one for which no work beyond the construction of each element in the set is required to prove that the element does indeed belong to \(A\), then we might reasonably expect the algorithm \(\mathcal{A}\) to be a choice function. In Martin-Löf’s type theory, every set is completely presented and, in keeping with the BHK interpretation, the axiom of choice is derivable.