Processing math: 100%
Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeMar 3rd 2014
    • (edited Mar 3rd 2014)

    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

    AdmRepeffKVAdmRepRT(𝒦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. Added reference

    Anonymouse

    diff, v10, current