[Agda] If all functions (N->N)->N are continuous, then 0=1.

[Martin Escardo]

   If all functions (N->N)->N are continuous, then 0=1.



Think of functions a : N -> N as sequences of natural numbers:

    a 0, a 1, a 2, a 3, ..., a n, ...

The "continuity axiom" for functions

     f : (N -> N) -> N,

that map sequences a : N -> N to numbers f(a), going back to Brouwer
in his intuitionistic mathematics in the early 20th century, says that
the value f(a) can depend only on a finite prefix of the infinite
argument a.

This makes sense computationally: there are no crystal balls in
computational processes, able to see and grasp the infinite input at
once. The input of f is computed bit-by-bit, in fact, often only when
f queries it.

After finitely many queries to its argument a : N -> N, the function f
is supposed to deliver its answer, if it's ever going to produce an
answer.

When this finiteness condition holds, we say that f is continuous
(never mind the reason for the terminology "continuous" in this message).

The link

   http://www.cs.bham.ac.uk/~mhe/continuity-false/continuity-false.html

writes down Brouwer's formulation of continuity in Agda notation, and
proves that:

   If all functions (N->N)->N are continuous, then 0=1.

What is going on? There is some discussion in the above link.

You may wish to read Andrej Bauer's related discussion
http://math.andrej.com/2011/07/27/definability-and-extensionality-of-the-modulus-of-continuity-functional/

The ideas of http://homotopytypetheory.org/book/ are relevant in this
respect too. To solve the apparent paradox, think about how one can
constructively prove existence without disclosing witnesses. Doubly
negated existence is too weak. One needs a stronger, constructive
notion of existence that deliberately doesn't exhibit witness, which
sometimes, but not always, can get to be disclosed. I attended a nice
talk by Thierry Coquand yesterday, in which he showed how the "axiom
of description" explains when and how the secret can be constructively
disclosed. In the HoTT book, this is explained as the axiom of unique
choice.

NB. Only the purest form of intensional Martin-Loef Type Theory is
used in the above Agda proof, and no universes are needed. No HoTT
axioms in particular.

Best, Martin