Skip to main content
added 894 characters in body
Source Link
Simon Henry
  • 42.4k
  • 5
  • 107
  • 205

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 pro-discrete 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.

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.

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 pro-discrete 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.

Source Link
Simon Henry
  • 42.4k
  • 5
  • 107
  • 205

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.