[Agda] If all functions (N->N)->N are continuous, then 0=1.
m.escardo at cs.bham.ac.uk
Thu Nov 28 14:59:44 CET 2013
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).
More information about the Agda