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

[Martin Escardo]

On 28/11/13 08:28, Altenkirch Thorsten wrote:
> Clearly, this formulation of continuity is inconsistent with functional
> extensionality because it makes it possible to observe an intensional
> property of a function - its modulus of continuity. What is surprising is
> that you manage to derive a contradiction w.o. using ext! So the wrong
> formulation of continuity doesn't even work in vanilla intensional Type
> Theory.

That's indeed one the points:

>> NB. Only the purest form of intensional Martin-Loef Type Theory is
>> used in the above Agda proof, and no universes are needed. No HoTT
>> axioms in particular.

(And no function extensionality in particular, as remarked in the
link.)

But the main point is that the interpretation Sigma of "exists" is not
always what we want (which is well known among a number of people).

Here is another (well known) example. If you define the image of a
function f : X -> Y to be

   im f = Sigma(y : Y).Sigma(x : X). f x = y,  (wrong),

then you get that im f is pointwise isomorphic to X. This is so even
if all elements of X are mapped to the same element y0 of Y. What one
needs is to hide some information, but not all:

   im f = Sigma(y : Y).||Sigma(x : X). f x = y||, (better),

The same is happening with continuity. The continuity witness (modulus
of continuity) should be kept secret if one wants to work sensibly
with continuity axioms.

But it is interesting to wonder what Brouwer meant when he formulated
this and other continuity axioms. Did he mean to use what we now call
Sigma?  This can't be, as one gets 0=1. But, on the other hand, the
constructive interpretation of exists as Sigma comes under the name
Brouwer-Heyting-Kolmogorov interpretation.

Martin