[Agda] Re: Classical Mathematics for a Constructive World

[Martin Escardo]

On 20/11/12 23:42, Liang-Ting Chen wrote:

> After Martin's reply, I just want to mention the following article by
> Per Martin-Löf which explains that the "extensional" choice / Zermelo's
> choice imply excluded middle in MLTT:
>
> Martin-Lof, 100 years of Zermelo's axiom of choice: what was the problem
> with it?,

Good that you mentioned that.

Let me then add more fuel to the general heated confusion about choice, 
and then try to clarify the situation.

In most toposes, the axiom of choice fails, simply because in any topos 
choice implies excluded middle, as toposes are mathematical models of 
intuitionistic set theory. And typically toposes fail badly regarding 
the validation of excluded middle, in trivial ways, even in the examples 
of toposes that have nothing to do with constructive mathematics.

Yet, any topos, being locally cartesian closed, is a model of Martin-Lof 
type theory, in which choice is a theorem. How come?

Contradiction. (?)

Of course not. In a topos, one has "exists" and "forall", and also 
"Sigma" and "Pi". Choice fails often when formulated for exists-forall, 
but always holds when formulated for Sigma-Pi.

One can say, loosely speaking: Any topos satisfies "Martin-Lof" choice, 
but hardly any topos satisfies "Set-theoretical" choice.

The so-called "Curry-Howard isomorphism" seems to say that exists-forall 
are the same as Sigma-Pi. They are not the same. In fact, homotopy type 
theory, if you are following this recent trend, is re-introducing the 
distinction in a constructive context, and even at a syntactic, 
model-independent, level.

In summary, choice may fail in its exists-forall formulation, but it 
always holds in its Sigma-Pi formulation (and rather trivially in both 
cases).

I hope this is not too cryptic.

Best,
Martin