Timeline for Does there exist a geometric morphism between the effective and topological topoi? Does one arise from synthetic topology?
Current License: CC BY-SA 4.0
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Apr 15 at 17:36 | vote | accept | Garrett Figueroa | ||
| Apr 14 at 15:28 | answer | added | Andrej Bauer | timeline score: 11 | |
| Apr 14 at 10:50 | comment | added | Ingo Blechschmidt | Here is a thing you could do, in lieu the geometric morphisms which likely don't exist/are trivial: Internally to the effective topos, you could construct a (suitable version of) the topological topos. That would basically amount to rereading the account of TT, but now not in a metatheory such as ZFC or IZF, but using Russian-style constructivism as the metatheory (with its formal Church–Turing thesis, every function $\mathbb{N} \to \mathbb{N}$ is Turing-computable). You could also do it the other way round. | |
| Apr 14 at 9:18 | comment | added | Andrej Bauer | I have a recollection of listening to a lecture by Peter Johnstone in which he stated that every geometric morphism from a Grothendieck topos to a ealizability topos factors trough Set. Or perhaps I got the directions reversed? Anyhow, you should stop looking for a geometric morphism of this kind and instead prove they're all trivial, or not even there. | |
| Apr 13 at 23:25 | comment | added | David Roberts♦ | To clarify slightly: every external function (i.e. in Set) $\mathbb{N}\to \mathbb{N}$ gives an endofunction on the NNO of $TT$. | |
| Apr 13 at 21:55 | comment | added | Simon Henry | There can't be a geometric morphism $f:Eff \to TT$ that's for sure. $f^*$ would preserve NNO (because $f^*$ always does) and as TT is a Grothendieck topos every function $N \to N$ is defined on the NNO of TT. But in EFF only computable functions acts on the NNO... | |
| S Apr 13 at 20:01 | review | First questions | |||
| Apr 13 at 20:02 | |||||
| S Apr 13 at 20:01 | history | asked | Garrett Figueroa | CC BY-SA 4.0 |