From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/7815 Path: news.gmane.org!not-for-mail From: Thomas Streicher Newsgroups: gmane.science.mathematics.categories Subject: Re: Reply to Eduardo Dubuc Date: Fri, 26 Jul 2013 22:08:59 +0200 Message-ID: References: Reply-To: Thomas Streicher NNTP-Posting-Host: plane.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii X-Trace: ger.gmane.org 1374970249 10877 80.91.229.3 (28 Jul 2013 00:10:49 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Sun, 28 Jul 2013 00:10:49 +0000 (UTC) Cc: categories@mta.ca, E D To: Marta Bunge Original-X-From: majordomo@mlist.mta.ca Sun Jul 28 02:10:52 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 1V3EZV-0005Fr-Tb for gsmc-categories@m.gmane.org; Sun, 28 Jul 2013 02:10:50 +0200 Original-Received: from mlist.mta.ca ([138.73.1.63]:54769) by smtp3.mta.ca with esmtp (Exim 4.80) (envelope-from ) id 1V3EX8-0000Jb-Nl; Sat, 27 Jul 2013 21:08:22 -0300 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1V3EX9-000459-Hm for categories-list@mlist.mta.ca; Sat, 27 Jul 2013 21:08:23 -0300 Content-Disposition: inline In-Reply-To: Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:7815 Archived-At: >> 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. >> >> 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. 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 [For admin and other information see: http://www.mta.ca/~cat-dist/ ]