From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/9044 Path: news.gmane.org!.POSTED!not-for-mail From: Sergey Goncharov Newsgroups: gmane.science.mathematics.categories Subject: Re: Predicativity in Categories Date: Thu, 1 Dec 2016 17:05:50 +0100 Message-ID: References: Reply-To: Sergey Goncharov NNTP-Posting-Host: blaine.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=windows-1252; format=flowed Content-Transfer-Encoding: 8bit X-Trace: blaine.gmane.org 1480617794 8781 195.159.176.226 (1 Dec 2016 18:43:14 GMT) X-Complaints-To: usenet@blaine.gmane.org NNTP-Posting-Date: Thu, 1 Dec 2016 18:43:14 +0000 (UTC) Cc: categories@mta.ca To: Steve Vickers Original-X-From: majordomo@mlist.mta.ca Thu Dec 01 19:43:09 2016 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from smtp3.mta.ca ([138.73.7.28]) by blaine.gmane.org with esmtp (Exim 4.84_2) (envelope-from ) id 1cCWK3-0001Zf-QE for gsmc-categories@m.gmane.org; Thu, 01 Dec 2016 19:43:07 +0100 Original-Received: from mlist.mta.ca ([138.73.1.63]:46606) by smtp3.mta.ca with esmtp (Exim 4.80) (envelope-from ) id 1cCWJg-0008K1-2a; Thu, 01 Dec 2016 14:42:44 -0400 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1cCWJg-0002Bj-Rb for categories-list@mlist.mta.ca; Thu, 01 Dec 2016 14:42:44 -0400 In-Reply-To: Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:9044 Archived-At: Dear Steve, thank you for your answer! Indeed, I was seeking for feedback in this style. Like you said, with the restrictions you adopt you are on a safe side, but those exclude function spaces, which are allowed in Martin-L?f TT, and the latter is commonly called predicative. I realize though that you have additional motivation for geometric logic (as a logic of observable properties, at least this is my current intuition, which I also picked up from your book) and that happens to be predicative. The reason I believe that one can potentially make sense of predicativity in categories is because I learned recently from the paper "Modular correspondence between dependent type theories and categories including pretopoi and topoi" by Maria Maietti that various classes of categories are uniformly described by their internal language written is the style of extensional dependent type theory. By incrementally extending the language one obtains narrower and narrower classes of categories ending up at toposes. Hence, I thought that there might be a way to formally classify such extensions as predicative or impredicative. Best regards, Sergey On 30/11/16 12:01, Steve Vickers wrote: > Dear Sergey, > > For myself, I'm not exactly sure I understand the original notion of > predicativity, but I have a rule of thumb that seems to work and > satisfy predicative mathematicians. I've frequently claimed that > parts of my work are predicative, and no one has complained so far. > > In topos theory, as you point out, the subobject classifier and > powersets indicate impredicativity. > > My rule of thumb is that "geometric" reasoning, preserved (up to > isomorphism) by the inverse image parts of geometric morphisms, is > safely within the predicative fragment. (Note that even exponentials, > function sets, are not geometric, so geometric reasoning is quite > restricted.) > > The subobject classifier and powersets are not geometric. > > On the other hand, the free semilattices, along with free algebras > (for cartesian theories) in general, are geometric, and they classify > Kuratowski finite subobjects. My rule of thumb predicts that > Kuratowski finite powersets are predicative, and there seems to be > general agreement with that. > > My current work on arithmetic universes seeks a setting for pure > geometric reasoning, without the non-geometric parts that exist in > toposes, and independent of base topos so long as it has an nno. > > Best wishes, > > Steve Vickers. > >> On 27 Nov 2016, at 18:53, Sergey Goncharov >> wrote: >> >> Dear Community, >> >> I am recently racking my brains in trying to understand what >> (im-)predicativity means from a categorical perspective, but >> failing short, hence calling for you help. >> ... >> Looking forward to your answers. >> >> Sergey >> [For admin and other information see: http://www.mta.ca/~cat-dist/ ]