Skip to main content
5 of 5
deleted 1 character in body
Andrej Bauer
  • 48.8k
  • 11
  • 131
  • 240

There is no geometric morphism $f : E \to F$ if $E$ is a realizaiblity topos and $F$ is a Grothendieck topos. Indeed, if we had such an $f$, then for any indexing set $I$, the topos $E$ would have the $I$-fold coproduct $\coprod_I 1$ of terminal objects: such a coproduct exists in $F$ and $f^*$ will carry it over to $E$, as it preserves the terminal object and coproducts. Taking $I$ to be the underlying pca of $E$ shows that this is impossible by a cadinality argument, see also the notion of width in Lemma 2.11 in Sheaf toposes for realizability, PDF here. Come to think of it, the paper might be of some independent interst to you.

Regarding the opposite direction, I once heard Peter Johnstone state that every geometric morphism from a Grothendieck topos to a realizability topos factors through $(\Gamma \dashv \nabla) : \mathsf{Set} \to \mathsf{RT}(A)$, but I cannot remember why (I was too young to understand much of Peter Johnstone anyway).

A topos that combines computability and topology in a particularly nice way is the Kleene-Vesley topos $\mathsf{RT}(\mathbb{N}^\mathbb{N}, (\mathbb{N}^\mathbb{N})_\mathsf{eff})$, and a slightly less nice one is $\mathsf{RT}(\mathcal{P}(\mathbb{N}), \mathsf{RE})$, see my PhD thesis or these unfinished notes on realizability.

Andrej Bauer
  • 48.8k
  • 11
  • 131
  • 240