25 Jul
2013
25 Jul
'13
9:33 p.m.
Your statement is valid internally in SS, that is once formalized in the internal language of the topos SS; this can be done in geometric logic, by considering a (possibly infinitary) disjunction over all the arrows f: C ---> X for C in CC (interpreted by the arrows Ff in SS) and existential quantifications. If you want a statement valid 'externally', you should instead use generalized elements in SS and epimorphic families involving their domains.
Since CC is internal to SS which is assumed as different from Set it doesn't make sense to consider an infinite disjunction over all arrows f: C --> X for C in CC. Thomas [For admin and other information see: http://www.mta.ca/~cat-dist/ ]