Added reference

- {#BauerSwan18} Andrej Bauer and Andrew Swan,
*Every metric space is separable in function realizability*, 2018, (arxiv:1804.00427)

Anonymouse

]]>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.

]]>