a tentative answer to Paul

a tentative answer to Paul

[Thomas Streicher]

Dear Paul,

I do have reveiled my meta-theory, namely ZFC together with the axiom that
every set appears as element of some Grothendieck universe. This is not a
question of belief but of convenience. I haven't found anything in category
theory which needs expressivity beyond that.

You ask what I mean by the validity of the statement

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

Well, it has to be read in the internal language of a topos augmented with
some `macros' form the language of dependent types (here X -> N is some map
in the topos and the formula specifies that it's the family P(N)_{n \in N}.
Of course, one might take the pains of Kripke-Joyaling this internal statement
BUT why should one want to do so.

You are quite right in emphasizing that specifying such a family is one
thing and its existence is another one. For the latter purpose one needs
the eaxiom of replacement though possibly not its full strength. That's the
motivation for my considerations in my "Universes in Toposes". Postulating
a class of display maps SS with a strongly generic family E -> U (i.e. this
map is in SS and all maps can be obtained as pullback of it) and some
desired closure properties. Now supposing N \in U and U being closed under
powerset P(-) its is a most simple exercise to construct a map  f : N -> U
with  f(0) = N  and  f(n+1) = P(f(n)). We have just exploited that P restricts
to a map U -> U. This is known since around 1970 when Martin-Loef introduced
universes. Of course, he now would not consider something impredicative as
the power set functor P but he would consider X \mapsto X^X as an operation
on U.

Apparently, quite a few category people are not that fond of universes in
this sense. So one may ask the question to which extent one may express
recursively defined families without universes. The answer given in Paul's
book is to require initial fixpoints of endofunctors on some category of
families. In case of the example above it would be an endofunctor on EE/N
where EE is the topos under consideration. (See
www.mathematik.tu-darmstadt.de/~streicher/itpowtop.pdf (temporary!)
for one possible way of putting it.)

Such an external handling of recursive family is certainly possible
but I find it inconvenient because I want to construct my recursive families
inside the internal language. In mathematics you never work externally but
always internally, i.e. in one single unspecified formal system like ZFC
or strengthenings of it (see above). "External" is a logician's idea who
considers formal systems, their models and relations between them. But when
doing mathematics it's not a good idea to "go external".

Thomas

PS I find interesting you comments about glueing and the necessity of
replacement. I haven't come across this because on the meta-level I use
a very strong system where I have it anyway. You are right that via glueing
you get a consistency proof for HAH (higher order arithmetic). But this
a priori doesn't require replacemnt since Zermelo set theory is sufficient
for this purpose.