Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I gather the following is true and is shown in Battenfield-Schröder-Simpson (pdf), but I haven’t really fully absorbed yet how $AdmRep$ is actually embedded in $RT(\mathcal{K}_2)$.
The subcategory on the effectively computable morphisms of the function realizability topos $RT(\mathcal{K}_2)$ is the Kleene-Vesley topos $KV$. The category of “admissible representations” $AdmRep$ (whose morphisms are computable functions (analysis), see there) is a reflective subcategory of $RT(\mathcal{K}_2)$ (BSS) and the restriction of that to $KV$ is $AdmRep_{eff}$
$\array{ AdmRep_{eff} &\hookrightarrow& KV \\ \downarrow && \downarrow \\ AdmRep &\hookrightarrow& RT(\mathcal{K}_2) }$
This is currently stated this way in the entry function ralizability and computable function (analysis), but please criticize/handle with care, I’ll try to further fine-tune as need be.
1 to 1 of 1