From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/7822 Path: news.gmane.org!not-for-mail From: David Roberts Newsgroups: gmane.science.mathematics.categories Subject: Re: Reply to Eduardo Dubuc Date: Mon, 29 Jul 2013 01:09:10 +0930 Message-ID: References: Reply-To: David Roberts NNTP-Posting-Host: plane.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable X-Trace: ger.gmane.org 1375100668 3271 80.91.229.3 (29 Jul 2013 12:24:28 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Mon, 29 Jul 2013 12:24:28 +0000 (UTC) To: "categories@mta.ca list" Original-X-From: majordomo@mlist.mta.ca Mon Jul 29 14:24:29 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 1V3mV2-0006eG-2F for gsmc-categories@m.gmane.org; Mon, 29 Jul 2013 14:24:28 +0200 Original-Received: from mlist.mta.ca ([138.73.1.63]:55340) by smtp3.mta.ca with esmtp (Exim 4.80) (envelope-from ) id 1V3mTo-0005yD-Cy; Mon, 29 Jul 2013 09:23:12 -0300 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1V3mTn-00025S-5d for categories-list@mlist.mta.ca; Mon, 29 Jul 2013 09:23:11 -0300 In-Reply-To: <20130728152016.GA23445@mathematik.tu-darmstadt.de> Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:7822 Archived-At: Hi, Since my answer on MathOverflow has been invoked a couple of times, let me expand on it a little. There is a notion of a topos being *constructively* well-pointed, which I learned from Mike Shulman (or rather, his paper Stack semantics and the comparison of material and structural set theories). This is the sort of thing that the category of CZF-sets has. And Mike proved that in the internal logic (in fact in an extension of the usual one, to cope with unbounded quantifiers), every topos is constructively well-pointed. Since Eduardo, at the beginning of his question stated that he was going to work in the internal logic of the base topos, I took this as given. Then one can reason as if one has an object * playing the r=C3=B4le of the point which picks out elements of 'sets'. The definition of epimorphism in the internal logic is just that any generalised element in the codomain lifts to the domain, and this reduces to checking for elements using *. The coproduct causes no trouble, being indexed by a 'set', and disjoint union doesn't go awry in the intuitionistic setting, by virtue of the fact coproducts are disjoint in a topos. To address the point about unbounded quantifiers, Mike gives the notion of a topos being *autological*, which means that in the internal logic one has unbounded separation, and so as much of set theory as one gets from e.g. ZF in the classical case. Given an autological base topos SS, all locally small cocomplete toposes over SS are autological, including unbounded ones. Mike might be able to answer more specific questions people have, but that is my line of reasoning. Best, David On 29 July 2013 00:50, Thomas Streicher wrote: > Dear David, > > indeed Michael's work is an alternative to the AST approach taylored > towards a setting where it is forbidden to speak of equality of sets. > He doesn't construct the category of classes around a topos but rather > works with Kripke Joyal semantics for it. > > Thomas [For admin and other information see: http://www.mta.ca/~cat-dist/ ]