trying to answer some of Paul's questions

trying to answer some of Paul's questions

[Thomas Streicher]

Dear Paul,

I am trying to answer at least some of your questions.

> what he might mean categorically by saying that
> an external family of objects is a function I -> Ob(EE) where I is a
> set unless his Ob(EE) is a "class" in either the sense of algebraic set
> theory (ie an object in another category besides EE) or some similar
> approach.

You can't say this "categorically" as far as I can see. I am working
informally on the meta-level and there both I and Ob(EE) are ome sets
and it is clear what is a function from I to Set. If necessary I can also
reveil the strength of my meta-level reasoning: ZFC plus the axiom that
every set appears as member of some Grothendieck universe.

> AST is an intellectually valid point of view on which much good
> category theory has been done in the past few years.  However,
> Mike Shulman and I would both like to know how one might formulate
> replacement WITHOUT classes.

Well, for the set theorist it's impossible anyway since he needs at
least the class V of all sets which, of course, is carefully hidden
as the (interpretation of the) single sort over which the variables
of the language of set theory range. Well, and by using first order
definable properties one has a lot of further classes not given official
status but which are there as interpretations of those formulas. That's
precisely the starting point of AST postulating a Heyting category EE
and a "universe" V in it which has enough properties for V being a model
of IZF. (Well, AST in its orginal form has also the ambition to construct
this class V as a quotient of a W-type.)

Only when reading your most recent mail it became clear to me that your
intentions are quite different from ETCS. McLarty's replacement axiom does
speak about external families which are syntactically definable in the
language of ETCS whereas you - as I understand it - want to stick to
internal families (aka display maps). The intention of my mail from Saturday
was to argue that the external notion of family is (at least) problematic
in a non-wellpointed context.

Using universes in toposes (as in my paper with this title) one can
formulate everything without using the external families and so one can
in AST.

> As I said before, they claim that replacement is necessary
> to construct the ordinal omega+omega, whilst this order structure can
> be constructed up to isomorphism very easily without it.

Of course, one can construct even larger prim.rec. orders but one
cannot prove their implementation as von Neumann ordinals. And that's
what they want.

> Thomas Streicher uses indexed/fibred category theory to link internal
> and external notions.  I don't see, however, how he manages to give
> the SPECIFICATION that a display map X-->N is the sequence of iterates
> of the powerset on N.  The formulation that I gave at the end of my
> previous posting and in Remark 9.6.16 in my book does do this.

But it's very easy to express this specification in the internal language
of a topos namely as

   \forall n:N \exists i : X_{n+1} -> P(X_n)  Iso(i)

>   the Artin gluing / Freyd cover / scone (Sierpinski cone) / logical
>   relations construction,  which can be used to prove CONSISTENCY
>   of various theories, once again by comparing the term model with
>   the ambient universe.

in PTJ's Elephant  3.6.3 (f) you find a description of sconing in a fibred
setting, i.e. over an arbitrary base: if p : EE -> SS is a geom. morph. then
sc_SS(EE) is just the glueing of  p_* : EE -> SS
that's my answer to the question of how I would define sconing relative
to an arbitrary base

this certainly doesn't answer you question above; I can just give an honest
answer: when using glueing I always used full power on the meta level including
the common identification of families of sets indexed by I and maps to I

asa far as AST is concerned there is no proof yet that models of AST are
stable under soning; a first attempt you can find in a paper by M. Warren

   Michael A. Warren.
   Coalgebras in a category of classes.
   Annals of Pure and Applied Logic, 146(1):60-71, 2007.

That's what Benno van den Berg just told me when asking him about it.

Sconing for the free topos with nno is of course not the issue here. But
to show that models of AST are stable under sconing is subtle. The key point
is that you seem to take for Set a big enough category containg a nontrivial
notion of small map. Otherwise there are problems to define an object of
small objects.

Thomas