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

[Martin Escardo]

On 28/11/13 08:28, Altenkirch Thorsten wrote:
> I am puzzled again!
>
> you manage to derive a contradiction w.o. using ext!

This has nothing to do with extensionality.

My one-sentence summary is this:

    Finding a continuity witness is a non-continuous operation.

No finite part of f:(N->N)->N is enough to find out which finite part
of a:N->N suffices to compute f(a).

The formulation of continuity, using Sigma, both

    (1) says that all functions are continuous, and
    (2) provides a continuity-witness-finder.

The proof of 0=1 works by defining a non-continuous function using the
hypothetical continuity-witness-finder (2), thus contradicting (1).

Martin