From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/7859 Path: news.gmane.org!not-for-mail From: Zhen Lin Low Newsgroups: gmane.science.mathematics.categories Subject: Re: A category internal to itself Date: Fri, 6 Sep 2013 09:20:30 +0100 Message-ID: References: <20130906080410.GA19753@mathematik.tu-darmstadt.de> Reply-To: Zhen Lin Low NNTP-Posting-Host: plane.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 X-Trace: ger.gmane.org 1378473218 25782 80.91.229.3 (6 Sep 2013 13:13:38 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Fri, 6 Sep 2013 13:13:38 +0000 (UTC) Cc: Andrej Bauer , categories list To: Thomas Streicher Original-X-From: majordomo@mlist.mta.ca Fri Sep 06 15:13:42 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 1VHvr4-00076Z-7i for gsmc-categories@m.gmane.org; Fri, 06 Sep 2013 15:13:42 +0200 Original-Received: from mlist.mta.ca ([138.73.1.63]:37762) by smtp3.mta.ca with esmtp (Exim 4.80) (envelope-from ) id 1VHvpl-0007td-5d; Fri, 06 Sep 2013 10:12:21 -0300 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1VHvpk-0000tE-1p for categories-list@mlist.mta.ca; Fri, 06 Sep 2013 10:12:20 -0300 In-Reply-To: <20130906080410.GA19753@mathematik.tu-darmstadt.de> Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:7859 Archived-At: On 6 September 2013 09:04, Thomas Streicher wrote: >> To begin, consider a category C with finite limits. Suppose C has an >> internal category U such that the externalisation of U as a C-indexed >> category (or category fibred over C) is equivalent to the >> self-indexing of C. Since U is locally small as a C-indexed category, >> the self-indexing of C has the same property, so we deduce that C is >> locally cartesian closed. > > Excellent observation! Thus C is a model for Martin-Loef type theory > with Type : Type (as interpreted by U). It is known since Girard's > paradox from 1970 that this type theory is inconsistent, i.e. that > every type is inhabited. Thus, in particular, all identity types are > inhabited which renders C trivial. I am aware of Girard's paradox but I was under the (mistaken?) impression that slightly more than the structure of a locally cartesian closed category was needed, e.g. a Prop type. > For a more categorical account of the inconcistency of type theory > with Type:Type see > > A note on Russell's paradox in locally cartesian > closed categories > Andrew M. Pitts & Paul Taylor > Studia Logica 48 (3):377 - 387 (1989) > > which is much simpler than Girard's original proof. Alex Simpson pointed out this paper to me yesterday. Thank you (to both of you!) for bringing it to my attention. > But I don't understand some of your subsequent arguments. > >> We have a universal fibration el U -> ob U (by restricting the >> fibration mor U -> ob U x ob U), so it follows that every object X >> admits a monomorphism X -> el U. > > why? and if so what is the point? in a topos for every object X there > is a mono 0 -> X Let X be an object. Then it has a name, say u : 1 -> ob U, and by pulling back u along the universal fibration el U -> ob U, we get a monomorphism X -> el U. This allows us to run Russell's argument in the internal logic, cf [McLarty, _Failure of cartesian closedness in NF_]. -- Zhen Lin [For admin and other information see: http://www.mta.ca/~cat-dist/ ]