Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorUrs
   • CommentTimeMar 3rd 2014
   • (edited Mar 3rd 2014)
   • PermaLink
   Author: Urs
   Format: MarkdownItexI gather the following is true and is shown in Battenfield-Schröder-Simpson ([pdf](http://ncatlab.org/nlab/files/BattenfeldDomains.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](#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.

   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.