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.
Best Answer
Let me wrote a quick introduction to this idea:
1) Locales
I do not know if you are already familiar with the notion of locale that Andrej is referring to in his talk: They are a small variation on the idea of a topological space, where instead of defining a space by giving a set of points together with a collection of "open subsets" stable under arbitrary unions and finite intersections, one just gives an abstract ordered set of "open subspaces" which should have arbitrary supremums and finite infimums and such that binary infinimum distribute over arbitrary supremum. Such a poset is called a Frame (this is actually the same as a complete Heyting algebra), a morphism of frame is an ordered preserving map which commutes to finite infimums and arbitrary supremums. And locales are defined as just being "the opposite of the category of frames", i.e. a locale is just a frame, and morphisms of locales are morphisms of frame in the other direction.
It is rather easy to go from a topological space to a locales by just remembering the poset of open subspaces, and attaching to a continuous map its action on open subset by pre-image. Conversely if one has a locale $X$, one can define a "point" of it as a morphism from the locale corresponding to the one point topological space to $X$, there is a topology on this set of points (generated by the element of the frame corresponding to $X$) and these two constructions form an adjunction between locales and topological spaces, which can be shown to be an equivalence between rather large subcategories. More precisely it induces an equivalence between "sober topological spaces" and "spatial locales", where spatial locales are the locales "having enough points" in a precise technical sense.
There are however some locales which have no points at all. At first you can regard them as pathological monster, but it in fact appears that at least some of them are extremely natural and interesting objects (things like the space of "generic real numbers" or "random real numbers" that Andrej mentioned in his talk, or the "space of bijection" between two infinite set of different cardinality whose non triviality is the key points for Cohen forcing to works).
Despite this, classically, locales and topological spaces are very similar (for example, if you are only interested in complete metric spaces or locally compact spaces you will not notice the difference) but the category of locales is overall (arguably) slightly better behaved than the category of topological spaces.
But constructively, it is a lot harder to construct "points" of locales and a lot more locale appears to be non-spatial. This make the gap between topological spaces and locales considerably larger. And in this weaker framework, locales become incredibly better behaved than topological spaces. For example without the law of excluded middle the correct definition of the locale of real number might be non-spatial but is always locally compact, while it is well known that constructively the topological space of real numbers can fail to be locally compact (this is one of the bad things that happen in constructive analysis that Andrej mentioned in his talk). In fact it is known that they agree if and only if the topological space of real number is locally compact.
Similarly, a lot of classical theorem which requiert the axiom of choices become fully constructive when formulated in terms of locales. This the case for example of the Tychonov theorem, the Hahn Banach theorem, or the Gelfand duality.
For example the idea for the Hahn Banach theorem is that instead of asking for the existence of certain linear form or extension of linear form, we construct a space (a locale) of linear form and show that this is not the empty space (even if it might not have points) and that the map between these spaces induced by restricting to a subspace is always a "surjection" in a good localic sense. And this roughly also what happen for the Gelfand duality or the case of ring spectrum that we will discuss below
I highly recommend to have a look to Peter Johnstone excellent non technical introduction paper to the subject "The point of pointless topology" which will expand on what I just said. and probably explains it more clearly.
2) The localic Zariski spectrum
So, the starting idea is that one can construct the Zariski spectrum of a ring, together with its structural sheaf directly as a locale without ever mentioning prime ideal or maximal ideal. For example, one can just says that the poset of open is given by the poset of radical ideal of the ring. One can also give a presentation by generator and relation of the corresponding frame which is more convenient to work with. This is done for example in section V.3 of P.T.Johnstone's book "Stone spaces". And while prime ideal are a little dangerous constructively as they might not exists, ideals are not problematic at all, you always have plenty of them.
This locale we are constructing is still morally the "space of prime ideal of the ring" but the question of whether the ring actually has any prime ideal or not become just the question of whether this space has points or not, which a rather unimportant question in locale theory.
In fact, if you are familiar with the notion of classifying topos, it is the "space of prime ideal" in the sense that it is the classifying space for prime ideal, more precesely for "prime ideal complement", i.e. subset $O$ of the ring such that ($xy \in O \Rightarrow x \in O \text{ and }y \in O$; $0 \notin O$; $1 \in O$ ; $x+y \in O \Rightarrow x \in O \text{ or } y \in O$) which classically are exactly the complements of prime ideal, and construcively are more important because they are the things you need to get a locale ring when localizing.
This let you go through with the definition of a scheme in a constructive setting. It appears than most classical results of algebraic geometry became constructive when formulated using locales instead of spaces (and replacing statement involving existence of prime or maximal ideal by statement about property of this "space of prime ideals" similarly to the Hahn banach theorem above). Unfortunately, except very basic things, these are mostly "folk theorem" and do not very often appears in literature (because let's face it, not many algebraic geometer are interested in constructivisme...). With the exception of the work of Ingo Blechschmidt that I mention below.
In fact (but that is a personal opinion) I've always found that, for someone already familiar with locale theory, the localic treatment of the basic property of the Zariski spectrum are notably simpler than their usual topological treatment.
3) Internal logic
The last step to this story relies on the use of "internal logic". The idea is that if you work internally in (the topos of sheaves over) the localic Zariski spectrum, then you actually have a "prime ideal of your ring" (more precisely, you have a "localizing system" which satisfies the properties to be the complement of a prime ideal mentioned above) and this prime ideal is in some sense the universal prime ideal of your ring (proving a property for this internal prime ideal proves property for all prime ideal of your ring) and a large number of proof that relies on the axiom of choice because they says at some point "let M be a maximal/prime ideal of your ring" (for example, if you prove that some element is nilpotent because it belongs to all prime ideal) become constructive if, instead of choosing a prime ideal, you move to this internal logic and use the universal one.
This produces a quite efficient and automatic method to make lots of results of algebra and algebraic geometry constructive.
This idea of exploiting internal logic in algebraic geometry tend to make everything constructive and has been pushed quite far by Ingo Blechschmidt (you can watch one of his talk here, or read his thesis work here)
To my knowledge the work of Ingo is the only place where you will find a non trivial treatment of algebraic geometry which use this picture.
For another example, another place, completely different from prime ideal, where you will use non-constructive things in algebra or algebraic geometry is when you want to talk about algebraic closure of a fields. But it appears that this point of view also provide a solution. In general you cannot construct a single algebraic closure of a given fields, but what you can instead do is to consider the "space of all algebraic closure of the field" in the sense of theory of classifying topsoes. This times this will not even be a locale, but a more general kind of topos, and it appears that this topos is something that have actually been studied a lot by algebraic geometers: indeed, if you start from some ring $R$ and study the "space of all algebraic closure of all residual fields of $R$" defined in a proper way what you get is nothing else than the "small étale topos of $R$". See the work of Gavin Wraith on the subject.