[Agda] If all functions (N->N)->N are continuous, then 0=1.
sanzhiyan at gmail.com
Wed Dec 4 07:22:43 CET 2013
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
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?
> Agda mailing list
> Agda at lists.chalmers.se
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Agda