From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/8949 Path: news.gmane.org!.POSTED!not-for-mail From: Steve Vickers Newsgroups: gmane.science.mathematics.categories Subject: New paper "Sketches for arithmetic universes" Date: Thu, 4 Aug 2016 17:23:16 +0100 Message-ID: Reply-To: Steve Vickers NNTP-Posting-Host: blaine.gmane.org Mime-Version: 1.0 (1.0) Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit X-Trace: blaine.gmane.org 1470407073 14251 195.159.176.226 (5 Aug 2016 14:24:33 GMT) X-Complaints-To: usenet@blaine.gmane.org NNTP-Posting-Date: Fri, 5 Aug 2016 14:24:33 +0000 (UTC) To: theory@cs.bham.ac.uk, categories@mta.ca Original-X-From: majordomo@mlist.mta.ca Fri Aug 05 16:24:25 2016 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from smtp3.mta.ca ([138.73.7.24]) by blaine.gmane.org with esmtp (Exim 4.84_2) (envelope-from ) id 1bVg2k-0008U7-OM for gsmc-categories@m.gmane.org; Fri, 05 Aug 2016 16:24:10 +0200 Original-Received: from mlist.mta.ca ([138.73.1.63]:47890) by smtp3.mta.ca with esmtp (Exim 4.80) (envelope-from ) id 1bVg1u-0005Bu-NW; Fri, 05 Aug 2016 11:23:18 -0300 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1bVg1i-0000rt-9M for categories-list@mlist.mta.ca; Fri, 05 Aug 2016 11:23:06 -0300 Original-Content-Transfer-Encoding: quoted-printable Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:8949 Archived-At: Some of you may have heard talks about my paper "Sketches for arithmetic uni= verses", or even seen preliminary drafts of it. I now have a version which I= intend to submit shortly, and have put it on my website at http://www.cs.bham.ac.uk/~sjv/AUSk.pdf I've also sent it to arXiv. The paper is intended to help deal with a problem with geometric logic, name= ly that it has infinities in its formalism (specifically: infinitary disjunc= tions) that are extrinsic to the logic itself and supplied by choosing a bas= e topos. In practice, many of the infinities needed are countable and are not sensiti= ve to change of base as long as the base has a natural numbers object. The a= im of this work is to make those infinities intrinsic to the logic by adding= type-theoretic ingredients (specifically, list objects, hence in particular= nnos) that enable infinite disjunctions to be replaced by existential quant= ification. Categorically this amounts to replacing Grothendieck toposes (ove= r base with nno) by arithmetic universes (no base needed) - that is to say, b= y pretoposes with parametrized list objects. Already, Milly Maietti has stud= ied some type-theoretic issues for these. The paper describes "contexts", finite gadgets analogous to sketches that pl= ay the role of geometric theories, and their classifying AUs, replacing clas= sifying toposes as generalized spaces. Maps and 2-cells for contexts are als= o finite gadgets. The 2-category of contexts embeds fully and faithfully in t= he 2-category of AUs, strict AU-functors, and natural transformations. Steve= [For admin and other information see: http://www.mta.ca/~cat-dist/ ]