Re: Reply to Eduardo Dubuc

[Thomas Streicher <streicher@mathematik.tu-darmstadt.de>]

>> 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/ ]