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.

2. • CommentRowNumber2.
   • CommentAuthornLab edit announcer
   • CommentTimeAug 29th 2024
   • PermaLink
   Author: nLab edit announcer
   Format: MarkdownItexAdded reference * {#BauerSwan18} [[Andrej Bauer]] and [[Andrew Swan]], *Every metric space is separable in function realizability*, 2018, ([arxiv:1804.00427](https://arxiv.org/abs/1804.00427)) Anonymouse <a href="https://ncatlab.org/nlab/revision/diff/function+realizability/10">diff</a>, <a href="https://ncatlab.org/nlab/revision/function+realizability/10">v10</a>, <a href="https://ncatlab.org/nlab/show/function+realizability">current</a>

   Added reference

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

   Anonymouse

   diff, v10, current