Dear Eduardo,
Thank you for keeping me au courant. Difficult as it is to write in my iPad, I want to tell you my position and what I think of your question.
My position (as that of any topos theorist) is that
1) If you work in an elementary topos SS, then it is true that you can do so "as in Sets", provided you do not use excluded middle ( as the internal logic is intuitionistic) or use Choice (as the set theory intrinsic to SS is constructive).
2) If on the other hand you work in a topos EE that is bounded over SS, then you cannot work "as in Sets" concerning constructions in EE that involve SS. Here it is necessary to resort to either the "teoria delle categorie sopra un topos di base" (indexed categories) or to the theory of fibrations.
Concerning your question, let me point out that, although you pretend to work entirely inside SS, you do not, as your construction involves EE. It certainly makes sense, since EE is locally small, and CC is small ( meaning internal to SS). What I want to warn you about is how you proceed from there without resorting to EE as a bounded SS- topos.
I apologize for previous (private) irrelevant remarks as I misunderstood your question - until now, that is.
Concerning Diaconescu's theorem, AC implies Booleaness can be done "as in Sets" but the proof is not trival. If you mean the theorem which gives a characterization of bounded SS-toposes as a classifying topos, it requires fibrations over SS.
Regards, Marta
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
2) If on the other hand you work in a topos EE that is bounded over SS, then you cannot work "as in Sets" concerning constructions in EE that involve SS. Here it is necessary to resort to either the "teoria delle categorie sopra un topos di base" (indexed categories) or to the theory of fibrations.
Concerning your question, let me point out that, although you pretend to work entirely inside SS, you do not, as your construction involves EE. It certainly makes sense, since EE is locally small, and CC is small ( meaning internal to SS). What I want to warn you about is how you proceed from there without resorting to EE as a bounded SS- topos.
I fully subscribe to this, That's what I also wanted to say but formulated less clearly. The saying that "toposes correspond to naive set theory without principle and excluded middle" is right only if "naive set theory" is identified with higher order logic. But in "naive category theory" you all the time have to quantify over families of objects and morphisms of a category where these collections don't form sets. In particular, you have to quantify over all objects of the base topos which you can't do inside the base topos. As Marta has said one has to resort to fibered/indexed reasoning which also cannot be (fully) expressed in the internal language of the base topos. As I wrote to Eduardo in a non-public mail I consider the "naive set theory" style arguments one often find in the literature as kind of "blueprints" for the precise fibered/indexed arguments. An alternative is using Algebraic Set Theory which allows one to build around every topos EE a category of classes in such a way that EE appears as internal to it. This, among other things, is the aim of a recent paper by Awodey, Butz, Simpson and myself which has is to appear at APAL and a preliminary version of which can be obtained from Alex's homepage (http://homepages.inf.ed.ac.uk/als/Research/Sources/set-models.pdf). Sorry for speaking pro domo but it is relevant here when one wants to fully stay within an internal language. Thomas [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
participants (2)
-
Marta Bunge -
Thomas Streicher