All texts I have read on settheoretic independence proofs consider several different sorts of constructions separately, such as Booleanvalued models (equivalently, forcing over posets), permutation models, and symmetric models. However, the topostheoretic analogues of these notions—namely topoi of sheaves on locales, continuous actions of groups, and combinations of the two—are all special cases of one notion, namely the topos of sheaves on a site. Is there anywhere to be found a direct construction, in the classical world of membershipbased set theory, of a "forcing model" relative to an arbitrary site?

Thanks to the comments by Joel Hamkins, it appears that there is an even more serious obstruction. In view of the main results of Grigorieff in Intermediate submodels and generic extensions in set theory, Ann. Math. (2) 101 (1975), it looks like the forcing posets are, up to equivalence, precisely the small sites (with the doublenegation topology) that preserve the axiom of choice in the generic extension. 


Are you familiar with this paper : Relating first order set theories and elementary toposes from Awodey,Butz,Simpson and Streicher. I haven't read in detail yet, but it really seems to provide a machinery that answer your question. I would also add that if such "general" theory as not been developed much is because (this is my personal opinion) it would be essentially useless: For model theorist, because of the various representation theorems for toposes and boolean toposes, it is know that all the eventual model of set theory you could get this way can be obtained by first taking a permutation model and then taking a boolean valued model model inside of it. What I mean is that any boolean Grothendieck topos is localic over the classyfing group of a prodiscrete topological group, and even worst, any Grothendieck topos satisfying the axiom of choice admit an etale covering by a boolean locale. And for topos theorist, well the main difference between a model of set theory and a topos is the possibility of comparing two arbitrary object for the membership relation, and I hardly see how this feature can be relevant for topos theory. 

