From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/9286 Path: news.gmane.org!.POSTED!not-for-mail From: Steve Vickers Newsgroups: gmane.science.mathematics.categories Subject: Re: Re: Algebraic closures and arithmetic universes Date: Thu, 03 Aug 2017 11:24:40 +0100 Message-ID: References: <845EEA81-985B-413B-9C39-1A911583E347@cs.bham.ac.uk> Reply-To: Steve Vickers NNTP-Posting-Host: blaine.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit X-Trace: blaine.gmane.org 1501776902 21618 195.159.176.226 (3 Aug 2017 16:15:02 GMT) X-Complaints-To: usenet@blaine.gmane.org NNTP-Posting-Date: Thu, 3 Aug 2017 16:15:02 +0000 (UTC) Cc: "categories@mta.ca list" To: droberts.65537@gmail.com Original-X-From: majordomo@mlist.mta.ca Thu Aug 03 18:14:56 2017 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from smtp2.mta.ca ([198.164.44.40]) by blaine.gmane.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ddIlp-0004fV-L0 for gsmc-categories@m.gmane.org; Thu, 03 Aug 2017 18:14:45 +0200 Original-Received: from mlist.mta.ca ([138.73.1.63]:40781) by smtp2.mta.ca with esmtp (Exim 4.80) (envelope-from ) id 1ddIlR-0002RP-He; Thu, 03 Aug 2017 13:14:21 -0300 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1ddIlH-0002GI-P2 for categories-list@mlist.mta.ca; Thu, 03 Aug 2017 13:14:11 -0300 In-Reply-To: Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:9286 Archived-At: Dear David, I'm sure there's scope for optimizing the AU axioms. In my "Sketches for AUs" I replaced the original list-arithmetic pretopos with a slightly different formulation that exploits the fact that, in the presence of list objects, the pretopos has all finite colimits. (This is essentially because one can form transitive closures of relations and hence get arbitrary coequalizers.) However, note that to use finitary W-types as internal structure (the way I described) you have to express "finitary" internally somehow; and to use them, or some of them, as external structure, with externally given A_i etc, you may need infinitely many operations to present the theory of AUs. My own feeling when I wrote "Sketches for AUs" was that the ugliest bits of the presentation were the exactness and stability conditions needed for a pretopos. (Look at the rules for exactness and stability in definition 15, for equivalence extensions.) I wondered whether they could be simplified in the presence of the list objects. All the best, Steve. On 03/08/2017 09:25, droberts.65537@gmail.com wrote: > Hi Steve, > > Ah, excellent. I do wonder then, if free parameterised list objects > are finitary (parameterised) W-types and all of the latter exist when > the former exist (in the presence of the other assumptions on the AU), > if existence of W-types is a cleaner assumption for an AU. It may be > like the definition of elementary topos, where terminal object, > pullbacks and power objects suffice, but people sometimes just package > (local) cartesian closedness into the definition (not to speak of > finite colimits) as it is perfectly equivalent. > > From a categorical point of view W-types may be ok, though for certain > parsimonious presentations I guess list objects may be smaller to > describe and so desirable for that reason. > [For admin and other information see: http://www.mta.ca/~cat-dist/ ]