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(𝒦2).
The subcategory on the effectively computable morphisms of the function realizability topos RT(𝒦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(𝒦2) (BSS) and the restriction of that to KV is AdmRepeff
AdmRepeff↪KV↓↓AdmRep↪RT(𝒦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.
Added reference
Anonymouse
1 to 2 of 2