From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/4345 Path: news.gmane.org!not-for-mail From: Thomas Streicher Newsgroups: gmane.science.mathematics.categories Subject: a tentative answer to Paul Date: Thu, 20 Mar 2008 14:22:19 +0100 (CET) Message-ID: NNTP-Posting-Host: main.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit X-Trace: ger.gmane.org 1241019884 12845 80.91.229.2 (29 Apr 2009 15:44:44 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 29 Apr 2009 15:44:44 +0000 (UTC) To: categories@mta.ca Original-X-From: rrosebru@mta.ca Thu Mar 20 11:20:02 2008 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 20 Mar 2008 11:20:02 -0300 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JcLcY-0006Xu-2O for categories-list@mta.ca; Thu, 20 Mar 2008 11:19:54 -0300 Original-Sender: cat-dist@mta.ca Precedence: bulk X-Keywords: X-UID: 109 Original-Lines: 58 Xref: news.gmane.org gmane.science.mathematics.categories:4345 Archived-At: 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.