From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/7852 Path: news.gmane.org!not-for-mail From: "Eduardo J. Dubuc" Newsgroups: gmane.science.mathematics.categories Subject: Re: A category internal to itself_correction Date: Wed, 04 Sep 2013 17:14:49 -0300 Message-ID: References: <52279262.4070909@dm.uba.ar> Reply-To: "Eduardo J. Dubuc" NNTP-Posting-Host: plane.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 7bit X-Trace: ger.gmane.org 1378385725 13040 80.91.229.3 (5 Sep 2013 12:55:25 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Thu, 5 Sep 2013 12:55:25 +0000 (UTC) Cc: Categories list To: Andrej Bauer Original-X-From: majordomo@mlist.mta.ca Thu Sep 05 14:55:25 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 1VHZ5p-000418-9p for gsmc-categories@m.gmane.org; Thu, 05 Sep 2013 14:55:25 +0200 Original-Received: from mlist.mta.ca ([138.73.1.63]:36123) by smtp3.mta.ca with esmtp (Exim 4.80) (envelope-from ) id 1VHZ4c-0007ph-P2; Thu, 05 Sep 2013 09:54:10 -0300 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1VHZ4b-0003Rs-N2 for categories-list@mlist.mta.ca; Thu, 05 Sep 2013 09:54:09 -0300 In-Reply-To: <52279262.4070909@dm.uba.ar> Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:7852 Archived-At: Where it says U[1, U'_0] = U_0 it should say U_0[1, U'_0] = U_0 On 04/09/13 06:23, Andrej Bauer wrote: > Chatting at a conference, the question came up why there is no > (non-trivial) category which is "internal to itself" (interpret this > in some sensible sense). And over coffee we thought this must be well > known, but not to us. Can somene shed some light on the matter? > > With kind regards, > > Andrej > Interesting and difficult question. Related to incompletness problems and diagonal arguments. Joyal considered arithmetic universes U (*), and an initial such U_0. (for example, for U = Sets: U_0[1, N] = standard Natural Numbers). Then show that within any arithmetic universe U you can construct internally a U_0. In particular U_0 exist (called U'_0) inside U_0. You have U[1, U'_0] = U_0. With this he proves Godel Incompletness. (*) A pretopos U such that admits free monoids: X \in U, X ---> M(X), in particular, N = M(0). (with this you have primitive recursive arithmetics and construct U_0). I sort of remember also that Penon considered a topos object E' internal to a topos E and such that E[1, E'] = E. It is a challenge to to fill all the technical details and make rigorous sense of all this. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]