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

[Andrea Vezzosi]

On Sun, Dec 1, 2013 at 10:24 PM, Martin Escardo <m.escardo at cs.bham.ac.uk>wrote:

> [...]
> Then the problem with the modulus-of-continuity functional is that it
> doesn't preserve limits (it is not continuous).
>
>
Does this mean that once we fix a modulus of continuity functional M we
should be able to find a sequence f_i of continuous functions converging to
g such that M f_i doesn't converge to M g? All without assuming M itself to
be continuous?

It could be an interesting example.



> If you want to know more, please feel free to ask. There are models of
> type theory (classical and constructive) based on the above ideas. One
> of them is Johnstone's topological topos. A closely related one,
> studied by Chuangjie and myself, admits a constructive treatment.
>
>
What's a good article to start from for the constructive model?


-- Andrea


> Best,
>
> 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/20131204/4f4b74cb/attachment.html