replacement and iterated powersets

[Paul Taylor <pt08@PaulTaylor.EU>]

Maybe I should wave my hands a bit less, and actually spell out a
concrete example.

Here is how you can say that the display map  X-->Nx2  in an elementary
topos with a natural numbers object is the sequence of iterated
powersets, starting with X[0,0]=N, where X[0,1] is the union of X[n,0].
In set-theoretic language, X is then the cardinal  beth_{omega.2}.

Of course, the following is not a CONSTRUCTION of this display map,
just a SPECIFICATION of it:  we need Replacement to say that there
EXISTS a display map that satisfies this specification.

First we define the strict arithmetical order on Nx2:
   (n,0) < (m,0)  if n < m
   (n,0) < (m,1)  always
   (n,1) < (m,1)  if n < m
   (n,1) < (m,0)  never
Nx2 is also a poset, with the reflexive order <= defined as < or =.

Let D(Nx2) be the lattice of lower subsets of Nx2 wrt <=.

Let  parse: Nx2 --> D(Nx2)  by  parse(p) = {q | q < p}.

Now let  X-->Nx2  be a discrete fibration in Pos.
This means that, whenever  q<=p,  there is a function  X[q]->X[p],
and this system respects identities and composition.

The powerset functor of the ambient elementary topos is fibred,
so we can construct another discrete fibration
    Y-->D(Nx2)
in which    Y[U] = colim {Y[q] | q in U}.

In particular,  if  U = parse (0,1) = { (n,0) | n in N },
Y[U] is the colimit of Y[n,0]  for  n in N  and the maps between them.

Now, we need to say that  Y[parse(p)] = X[p], up to isomorphism.

But this is just the statement that

     X  --------->  Y
     |    |         |
     |    |         |
     |----+         |
     |              |
     |              |
     V   parse      V
    Nx2 -------> D(Nx2)

is a pullback.

Paul Taylor