From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/7816 Path: news.gmane.org!not-for-mail From: "Eduardo J. Dubuc" Newsgroups: gmane.science.mathematics.categories Subject: Re: Reply to Eduardo Dubuc Date: Fri, 26 Jul 2013 18:44:12 -0300 Message-ID: References: <20130726200858.GB32154@mathematik.tu-darmstadt.de> Reply-To: "Eduardo J. Dubuc" NNTP-Posting-Host: plane.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit X-Trace: ger.gmane.org 1374970310 11437 80.91.229.3 (28 Jul 2013 00:11:50 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Sun, 28 Jul 2013 00:11:50 +0000 (UTC) Cc: Marta Bunge , categories@mta.ca To: Thomas Streicher Original-X-From: majordomo@mlist.mta.ca Sun Jul 28 02:11:53 2013 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from smtp3.mta.ca ([138.73.1.186]) by plane.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1V3EaW-0005kd-MT for gsmc-categories@m.gmane.org; Sun, 28 Jul 2013 02:11:52 +0200 Original-Received: from mlist.mta.ca ([138.73.1.63]:54775) by smtp3.mta.ca with esmtp (Exim 4.80) (envelope-from ) id 1V3EY1-0000MW-SK; Sat, 27 Jul 2013 21:09:17 -0300 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1V3EY2-00046H-Rl for categories-list@mlist.mta.ca; Sat, 27 Jul 2013 21:09:18 -0300 In-Reply-To: <20130726200858.GB32154@mathematik.tu-darmstadt.de> Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:7816 Archived-At: On 26/07/13 17:08, Thomas Streicher wrote: >>> 2) If on the other hand you work in a topos EE that is bounded >>> over SS, then you cannot work "as in Sets" concerning >>> constructions in EE that involve SS. Here it is necessary to >>> resort to either the "teoria delle categorie sopra un topos di >>> base" (indexed categories) or to the theory of fibrations. >>> >>> [[1===1]] >>> Concerning your question, let me point out that, although you >>> pretend to work entirely inside SS, you do not, as your >>> construction involves EE. It certainly makes sense, since EE is >>> locally small, and CC is small ( meaning internal to SS). What I >>> want to warn you about is how you proceed from there without >>> resorting to EE as a bounded SS- topos. > > I fully subscribe to this, That's what I also wanted to say but > formulated less clearly. > > The saying that "toposes correspond to naive set theory without > principle and excluded middle" is right only if "naive set theory" > is identified with higher order logic. But in "naive category > theory" you all the time have to quantify over families of objects > and morphisms of a category where these collections don't form sets. > In particular, you have to quantify over all objects of the base > topos which you can't do inside the base topos. > > As Marta has said one has to resort to fibered/indexed reasoning > which also cannot be (fully) expressed in the internal language of > the base topos. > > [[2===2]] > As I wrote to Eduardo in a non-public mail I consider > the "naive set theory" style arguments one often find in the > literature as kind of "blueprints" for the precise fibered/indexed > arguments. > > An alternative is using Algebraic Set Theory which allows one to > build around every topos EE a category of classes in such a way that > EE appears as internal to it. This, among other things, is the aim of > a recent paper by Awodey, Butz, Simpson and myself which has is to > appear at APAL and a preliminary version of which can be obtained > from Alex's homepage > (http://homepages.inf.ed.ac.uk/als/Research/Sources/set-models.pdf). > > Sorry for speaking pro domo but it is relevant here when one wants > to fully stay within an internal language. > > Thomas Thanks Marta an Thomas, I am learning a lot !. I would like to comment in the items marked [[1===1]] and [[2===2]] of your answers. It seems to me now that the argument in my question does not need any theory of indexing categories. See, concerning [1===1] above I can say: My construction does not involve EE. It involves an internal site CC in SS, a functor CC ---> SS, a coproduct in SS indexed by an object in SS, and a SINGLE object X in EE, which is sheaf CC^op ---> SS. All this involves ONLY SS, and no forbiden quantifications are used. So the internal logic of SS should suffice. Concerning [2===2], you are probably right in many cases, precisely cases that I distrust because I feel the authors are not carefully enough (this due to my ignorance together with a tendency to be as Saint Thomas, "have to see to belive"). But in other cases not. For example, the entire paper Joyal-Tierney, An extension of the galois theory of grothendieck, Memoirs 309, is no "blue print" for nothing, it is in final form, very careful, and entirely justified (even their change of base) without any need of fibered/indexed arguments, as they say, (e.g. Boileau-Joyal) suffices. For example, they consider p: EE ---> SS, and say p_* sends sup-lattices to sup-lattices, they consider a left adjoint p^# (between the categories of sup-lattices) and stablish an isomorphism Hom(L, p_*(M)) = p_*Hom(p^#(L), M) in SS and say "expresses the (strong) adjointness p^# --| p_*" (page 44). They use "strong", no mention at all to "indexed adjoint", and this isomorphism is just a definition of strong. But, is not true that a topos p: EE ---> SS is canonically indexed and that for many things you can proceed tacitly without need to mention any theory of indexed categories ?. Even for constructions in EE ?. For example, a family in EE indexed by I in SS is just an arrow X ---> p*I, and the COPRODUCT_{i \in I} X_i in EE is just X. Please, do not think I am against fibered/indexed arguments, I can not be either against or in favor, since I do not know the theory. After your answers I understand now the theory is useful when you need to use quantifications not avaiable in the internal logic of a topos and other things of this sort. Best Eduardo. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]