A topos for realizability under a variable oracle

Question

I am looking for a topos that describes realizability by Turing machines with access to a “variable oracle”.

I think the construction I want is this. Start with Baire space $\mathcal{N} := \mathbb{N}^{\mathbb{N}}$ (or Cantor space $\mathcal{C} := 2^{\mathbb{N}}$) with its usual topology¹, and consider the topos $\mathbf{Sh}_X$ of sheaves on $X := \mathcal{N}$ (or $\mathcal{C}$). Let $x$ be the identity function on $X$ which we consider as an element of Baire/Cantor space internally in $\mathbf{Sh}_X$ (the “variable oracle”² in question). Now consider the “Kleene first algebra with $x$ as oracle” $\mathcal{K}_1^x$ internally in $\mathbf{Sh}_X$, that is, the natural numbers object of $\mathbf{Sh}_X$ (sheaf of locally constant $\mathbb{N}$-valued functions on $X$) seen as labels for Turing machines with $x$ as oracle and application of Turing machines as composition law (everything done internally in $\mathbf{Sh}_X$). Finally, consider the realizability topos for $\mathcal{K}_1^x$, constructed just as the effective topos is constructed from $\mathcal{K}_1$ (that is, a realizability topos) but for the PCA $\mathcal{K}_1^x$ and internally in $\mathbf{Sh}_X$.

However, this description is a bit sketchy (especially the part constructing a realizability topos internally in a sheaf topos), and I'm afraid I may have missed some subtleties that could cause the construction to go wrong or not behave as I expect. Even if nothing goes wrong, maybe there's a simpler (more direct) way to describe the resulting topos than a two-step construction as I sketched. Rather than check the details myself, I'd first like to know if someone already did this.

So, question: has the topos suggested above been considered before? If so, is there a more economical way to present it? Are there any significant pitfalls in the construction I sketched?

1. Of course, many other things may be of interest here, like using the density topology instead of the usual topology, and/or replacing $X$ by its booleanization (viꝫ. the locale associated with the Boolean algebra of regular open sets). I hope the construction isn't sensitive to this sort of things!

2. The word “generic” might be used here, but I wonder if it's not best to reserve its use for the Boolean case (as defined in the previous footnote).

Answer 1

I haven't seen this exact topos studied in the literature, but it's a sensible notion and quite similar to the toposes used in Goodman's theorem and De Jongh's theorem (Section 4.6.2 in Van Oosten, Realizability: An Introduction to its Categorical Side). In Goodman's theorem the topos is similarly constructed as the realizability topos on $\mathcal{K}_1^f$ where $f$ is a generic element of Cantor space added in a sheaf topos, although the sheaf topos is presented in terms of forcing rather than topology. I can't think of any applications of just working in Cantor space without modification, so that might be why it hasn't been considered, but you can also consider variations where you carefully choose subspaces of Cantor space with particular properties, with the same idea. There's an interesting feature of these toposes that you can nicely describe the logic in a way that combines forcing notation with realizability: given a finite sequence of numbers $\sigma$ (i.e. basic open in Cantor space), a natural number $e$, and a sentence $\phi$, you can define $e \Vdash_\sigma \phi$ to be "$\sigma$ forces $e$ to realize $\phi$" or less formally, "$e$ realizes $\phi$ at $\sigma$."