From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/4337 Path: news.gmane.org!not-for-mail From: Colin McLarty Newsgroups: gmane.science.mathematics.categories Subject: Re: categorical formulations of Replacement Date: Wed, 19 Mar 2008 09:02:51 -0400 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 1241019880 12810 80.91.229.2 (29 Apr 2009 15:44:40 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 29 Apr 2009 15:44:40 +0000 (UTC) To: Categories list Original-X-From: rrosebru@mta.ca Wed Mar 19 15:18:53 2008 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 19 Mar 2008 15:18:53 -0300 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1Jc2nk-0001Ir-Pu for categories-list@mta.ca; Wed, 19 Mar 2008 15:14:12 -0300 Content-Disposition: inline Original-Sender: cat-dist@mta.ca Precedence: bulk X-Keywords: X-UID: 101 Original-Lines: 61 Xref: news.gmane.org gmane.science.mathematics.categories:4337 Archived-At: Paul Taylor Wednesday, March 19, 2008 8:05 am Writes > I really do not have much idea of what you mean by statements like > \forall n:N \exists i : X_{n+1} -> P(X_n) Iso(i). > Nor do I understand similar statements to this in either > "An elementary theory of the category of sets (extended version)" > or "Exploring categorical structuralism" > by Bill Lawvere and Colin McLarty respectively. As to replacement in ETCS: ETCS is formulated in the first order language (with equality) of category theory. Take it as a one-sorted language (arrows) with composition C(g,f;h). It makes no principled difference for our purposes but is extremely handy to also assume constants 1 of set type (axiomatized as terminal) and "true" of function type (axiomatized as an element of a truth value set) and partially defined operators for say, pullbacks and the evaluation functions for function sets. ZF is formulated in the first order language (with equality) with set-membership epsilon. Replacement in ETCS like replacement in ZF is an axiom scheme positing one axiom for each formula of a certain form in the first order language of the theory. ZF-replacement posits one quantified axiom for each formula Rxy with two free variables (necessarily variables over sets, since that is what ZF has, and if you like you may allow other variables as parameters). The axiom for Rxy says "For any set S, if R relates each element x\in S to a unique set y then there is a set X whose elements are exactly those sets y that are R-related to some x\in S." ETCS posits one quantified axiom for each formula Rfy with f of arrow type (the axiom will say f has domain 1 so f stands for some element of a set) and y of set type. The axiom for Rfy says "For any set S, if R relates each function f:1-->S to a set y unique up to isomorphism then there is an S-indexed set of sets X-->S where the fiber over each x is isomorphic to the related set y." The apparatus of discrete fibrations applies here and no doubt to good advantage for serious work. But very little is needed in stating the axiom scheme. Let me say again that my account of replacement is just Bill's from 1965 only cast as replacement rather than reflection since people are far more familiar with replacement (and using the simplifications to ETCS that came with elementary topos theory). Colin