According to the BHK interpretation of intuitionistic logic we have that:
- A proof of $\exists x \in A . \phi(x)$ consists of a pair $(a, p)$ where $a \in A$ and $p$ is a proof of $\phi(a)$.
- A proof of $\forall x \in A . \phi(x)$ is a method which takes as input $a \in A$ and outputs a proof of $\phi(a)$.
- A proof of $\psi \Rightarrow \xi$ is a method which takes proofs of $\psi$ to proofs of $\xi$.
Here "method" should be understood as an unspecified, pre-mathematical notion. It could be algorithm, or continuous map, or mental process, or Turing machine, etc.
The axiom of choice can be stated, for any sets $A$, $B$ and relation $\rho$ on $A \times B$, as:
\begin{equation}
(\forall x \in A . \exists y \in B . \rho(x,y))
\Rightarrow
(\exists f \in B^A . \forall x \in A . \rho(x, f(x)).
\tag{AC}
\end{equation}
This is equivalent to the usual formulation (exercise, or ask if you do not see why). Let us unravel what it means to have a proof of the above principle. First, a proof of
$$\forall x \in A . \exists y \in B . \rho(x,y) \tag{1}$$
is a method $C$ which takes as input $a \in A$ and outputs a pair $$C(a) = (C_1(a), C_2(a))$$ such that $C_1(a) \in B$ and $C_2(a)$ is a proof of $\rho(a, C_1(a)).$ Second, a proof of
$$\exists f \in B^A . \forall x \in A . \rho(x, f(x)) \tag{2}$$
is a pair $(g, D)$ such that $g$ is a function from $A$ to $B$ and $D$ is a proof of $\forall x \in A . \rho(x, g(x))$.
Therefore a proof of (AC) above is a method $M$ which takes the method $C$ which proves (1) and outputs a pair $(f, D)$ which proves (2). Is there such an $M$? It looks like we can take $f = C_1$ and $D = C_2$, and viola the axiom of choice is proved constructively! Well, not quite. We were asked to provide a function $f : A \to B$ but we provided a method $C_1$. Is there a difference? That depends on the exact meaning of "method" and "function". There are several possibilities, see below.
The important thing is that now we can understand what Bishop meant by "a choice is implied by the very meaning of existence". If we ignore the difference between "method" and "function" then under the BHK interpretation choice holds because of the constructive meaning of $\exists$: to exist is to construct, and to construct a $y \in B$ depending on $x \in A$ is to give a method/function that constructs, and therefore chooses, for each $x \in A$ a particular $y \in B$.
It remains to consider whether a "method" $C_1$ taking inputs in $A$ and giving outputs in $B$ is the same thing as a function $f : A \to B$. The answer depends on the exact formal setup that we use to express the BHK interpretation:
Martin-Löf type theory
In Martin-Löf type theory there is no difference between "method" and "function", and therefore choice is valid there (but the exact argument outlined above).
Bishop constructive mathematics
In Bishop constructive mathematics a set is given by an explanation of how its elements are constructed, and when two such elements are equal. For instance, a real number is constructed as sequence of rational numbers satisfying the Cauchy condition, and two such sequences are considered equal when they coincide in the usual sense. This means, in particular, that two different constructions may represent the same element (both $n \mapsto 1/n$ and $n \mapsto 2^{-n}$ represent the real number "zero").
Now, importantly, we distinguish between operations and functions. The former is a mapping from a set $A$ to a set $B$, and the latter a mapping which respects equality (we say that it is extensional). To see the difference, consider the operation from $\mathbb{R}$ to $\mathbb{Q}$ which computes from a given $x \in \mathbb{R}$ a rational $q \in \mathbb{Q}$ such that $x < q$: since $x$ is a Cauchy sequence, we may take $q = x_i + 42$ for a large enough $i$ (which can be determined explicitly once we make our definition of reals a bit more specific). The operation $x \mapsto q$ does not respect equality: by taking a different Cauchy sequence $x'$ which represents the same real, we get a rational upper bound $q'$ which is not equal to $q$. In fact, in Bishop constructive mathematics it is impossible to construct an extensional operation that computes rational upper bounds of reals.
In Bishop constructive mathematics method is understood as operation, and function as extensional operation. Choice is then valid only in some instances, but not in general. In particular, if $A$ has the property that every element is canonically represented by a single construction, then every operation from $A$ to $B$ is automatically extensional, and choice from $A$ to $B$ is valid. An example is $A = \mathbb{N}$ because each natural number is represented by precisely one construction: $0$, $S(0)$, $S(S(0))$, ...
The moral of the story is that the devil hides important details in the passage from informal, pre-mathematical notions to their mathematically precise formulation.
