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

[Andrea Vezzosi]

On Thu, Nov 28, 2013 at 2:59 PM, Martin Escardo <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?


Andrea


> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20131130/3baeace1/attachment-0001.html