<div dir="ltr">On Thu, Nov 28, 2013 at 2:59 PM, Martin Escardo <span dir="ltr"><<a href="mailto:m.escardo@cs.bham.ac.uk" target="_blank">m.escardo@cs.bham.ac.uk</a>></span> wrote:<br><div class="gmail_extra"><div class="gmail_quote">
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="im"><br></div>
My one-sentence summary is this:<br>
<br>
Finding a continuity witness is a non-continuous operation.<br>
<br>
No finite part of f:(N->N)->N is enough to find out which finite part<br>
of a:N->N suffices to compute f(a).<br>
<br></blockquote><div><br></div><div>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?</div>
<div><br></div><div><br></div><div>Andrea<br></div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
The formulation of continuity, using Sigma, both<br>
<br>
(1) says that all functions are continuous, and<br>
(2) provides a continuity-witness-finder.<br>
<br>
The proof of 0=1 works by defining a non-continuous function using the<br>
hypothetical continuity-witness-finder (2), thus contradicting (1).<div class="HOEnZb"><div class="h5"><br>
<br>
Martin<br>
______________________________<u></u>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a><br>
</div></div></blockquote></div><br></div></div>