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

[Martin Escardo]

On 30/11/13 02:10, Andrea Vezzosi wrote:
> On Thu, Nov 28, 2013 at 2:59 PM, Martin Escardo <m.escardo at cs.bham.ac.uk
> <mailto:m.escardo at cs.bham.ac.uk>> wrote:
>
>
>     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).
>
>
> What would be an explicit definition of "finite part" for elements of (N
> -> N) -> N? Or, in other words, what's a good intuition for the topology
> of that type?

Sorry, I missed this question.

The topology of the type (N->N)->N is rather complicated in terms of
open sets. In terms of finiteness, an approach using domain theory is
natural, but requires a number of definitions and proofs before we can
say it.

Moreover, it is hard to formulate such things
constructively. Chuangjie Xu and I have done some work on this.

If you ignore constructivity, which can be useful for a rough (and
distorted) understanding, it is easier to think in terms of
convergent sequences. We say that a sequence f_i in (N->N)->N
converges to g if whenever a sequence a_i in N->N converges to b, then
the sequence f_i(a_i) converges to g(b).

So you still need to explain convergence in N->N. We say that a
sequence a_i in N->N convergers to b if for every n there is j such
that all a_i, for i>=j, agree with b in the first n positions.

Then the problem with the modulus-of-continuity functional is that it
doesn't preserve limits (it is not continuous).

If you want to know more, please feel free to ask. There are models of
type theory (classical and constructive) based on the above ideas. One
of them is Johnstone's topological topos. A closely related one,
studied by Chuangjie and myself, admits a constructive treatment.

Best,
Martin