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