Timeline for Can we internalize topological fixed point theorems in an effective topos?
Current License: CC BY-SA 3.0
6 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Feb 20, 2022 at 20:09 | comment | added | Andrej Bauer | @JamesHanson: arxiv.org/abs/1902.07366 | |
| Feb 20, 2022 at 19:50 | comment | added | James E Hanson | @AndrejBauer Ingo mentions that there is an intuitionistic proof that the MacNeille reals are uncountable. Is this written down somewhere? | |
| Feb 20, 2022 at 19:09 | comment | added | Andrej Bauer | @JamesHanson: If you are referring to my comment, then yes, see this thread for a summary of what is known. | |
| Feb 20, 2022 at 17:23 | comment | added | James E Hanson | @AndrejBauer Is this still open? | |
| Dec 1, 2017 at 13:20 | comment | added | Andrej Bauer | If you can find a topos in which there is an internal surjection $\mathbb{N} \to [0,1]$ then you will solve the open problem "can there be a topos with an internal surjection $\mathbb{N} \to \mathbb{R}$", and in fact such a topos will be rather amazing. It cannot satisfy countable choice (because countable choice implies there is no surjection $\mathbb{N} \to [0,1]$), so realizability toposes are not going to work. It cannot be a Boolean topos for the same reason. I looked but couldn't find it, nor do I have a proof that it doesn't exist. | |
| Nov 16, 2017 at 23:18 | history | asked | Sam Eisenstat | CC BY-SA 3.0 |