[Agda] If all functions (N->N)->N are continuous, then 0=1.
sanzhiyan at gmail.com
Sat Nov 30 03:10:14 CET 2013
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
> 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).
> Agda mailing list
> Agda at lists.chalmers.se
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Agda