Re: Reply to Eduardo Dubuc

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

Dear Eduardo,

let's carefully look how internal to SS your statement is. You start
from a bounded geometric morphism F -| U : EE -> SS and an object X of EE.
What ensures your claim is that there is a diagram (in EE)

             e
       X <<--- u^*G -----> G
                 |         |
                 |   p.b.  |
                 V         V
                 FJ ----> FI
                     Fu

where G --> FI is a generic family for P_F (the fibered topos
associated with F : SS -> EE). Here you have an EXTERNAL existential
quantification over J, u  and e. But using local smallness of P_F you
can concretely witness J as \coprod_{i \in I} hom_EE(G_i,X) and u as
first projection on I. From this you also get e. But that means that
one proves the statement on the metalevel which allows one to speak
about SS, EE and functors between them.

In particular, you have to argue how you can express within SS that e
(a morphism of EE) is epic. How can you do this in the internal language
of SS? You have to quantify over arbitrary maps in EE with source X.

Moreover, you do not want to have your claim valid for just a single
particular external X in EE but you want to have it "for all X in EE".
Kripke-Joyaling this amounts to considering all external families
a : A --> FK (as on p.51 of Marta and Jonathon's book though they use
different letters).

There is some possibility of giving a coherent account of this. If you
have your base topos SS then split fibrations over SS are the same as
categories internal to Psh(SS) (where Psh(SS) = Set^{SS^op} for Set
big enough to contain SS as an internal category). Now you can reason
in the internal language of Psh(SS) but not in the internal language of SS.
That I have learnt from B'enabou some years ago but it's unpublished
(as usual). Now the problem is that Psh(SS) is too weak a logic and
one might want to work rather in sheaves over SS w.r.t. regular cover
topology.

In the work of Awodey, Forssell and Warren on their variant of algebraic
set theory (http://www.phil.cmu.edu/projects/ast/Papers/afw_06.pdf) this is
preformed to some extent. They consider Idl(SS), the "ideal completion of SS"
within which SS appears as a small category.

Best regards, Thomas


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]