My understanding is that forcing (such as Cohen forcing) can be described via a topos. For example this [nlab article on forcing][1] describes forcing as a "the topos of sheaves on a suitable site." My question concerns forcing in computability theory, for example as described in Chapter 3 or these [lecture notes of Richard Shore][2]. The idea is that the generics are those which meet all *computable* dense sets of forcing conditions. (Computable can mean a few things. Often it is taken to mean a $\Sigma^0_1$ set of forcing conditions. Also, usually the forcing posets are countable.) Since there are only countably many such dense sets, such effective generics exist. >Is there a known/canonical type of topos corresponding to the forcing in computability theory? Any references would be appreciated. *FYI: My background is in computability theory, proof theory, and computable analysis. I know little about topos theory, but I am willing to learn a bit. I am mostly asking this question because I want to compare some ideas I have about effective versions of Solovay forcing with some work by others about the topos corresponding to Solovay forcing. Also, it is always nice to learn new things.* [1]: http://ncatlab.org/nlab/show/forcing [2]: http://www.math.cornell.edu/~shore/papers/pdf/SingLect2NS.pdf