My understanding is that forcing (such as Cohen forcing) can be described via a topos. For example this nlab article on forcing 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. 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.
