From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/7860 Path: news.gmane.org!not-for-mail From: Andrej Bauer Newsgroups: gmane.science.mathematics.categories Subject: Re: A category internal to itself Date: Fri, 6 Sep 2013 11:48:52 +0200 Message-ID: References: Reply-To: Andrej Bauer NNTP-Posting-Host: plane.gmane.org Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable X-Trace: ger.gmane.org 1378473296 26530 80.91.229.3 (6 Sep 2013 13:14:56 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Fri, 6 Sep 2013 13:14:56 +0000 (UTC) To: Thomas Streicher , categories list Original-X-From: majordomo@mlist.mta.ca Fri Sep 06 15:14:59 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 1VHvsJ-0007a0-Bi for gsmc-categories@m.gmane.org; Fri, 06 Sep 2013 15:14:59 +0200 Original-Received: from mlist.mta.ca ([138.73.1.63]:37768) by smtp3.mta.ca with esmtp (Exim 4.80) (envelope-from ) id 1VHvrH-0008FY-AE; Fri, 06 Sep 2013 10:13:55 -0300 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1VHvrG-0000vw-Af for categories-list@mlist.mta.ca; Fri, 06 Sep 2013 10:13:54 -0300 In-Reply-To: Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:7860 Archived-At: I would like to thank everyone for so many wonderful answers. It seems that there is an "easy" case and a "difficult" case. In the easy case we look at the global points of the internal category and expect to see the external category. This can be arranged so that the category is even a topos (the free one), as explained by Peter Johnstone. And there are other possibilities, such as the arithmetical universe. The difficult case involves looking at general points, which leads to questions about fibrations. As we know from Andy Pitts and Paul Taylor, an lccc which is internal in the stronger sense is trivial. But I wonder if there is a category C which contains a universal object U such that Hom(-, U) gives a model of dependent type theory (without identity types!) which is the same as some fibration involving C. What I have in mind is the following (I will speak indexly instead of fibrantly). Consider a cartesial-closed category Dom of domains containing a universal object U in the sense that every other object is a retract of U. For instance, to keep everything very pretty we could take countably-based algebraic lattices, in which P(=E2=8D=B5) is universal. For each domain D in Dom we have the continuous functors Cont(D, Dom), a la Ulrich Bergers Habilitationschrift, that gives an indexed category. But such functors ought to correspond closely to the continuous maps D -> U because the elements of U rerpesent retracts of U which are the object of Dom. All of this needs to be massaged a bit, and before I do it, I would prefer to hear whether I am reinventing the wheel. The results would be a model of type theory (with =CE=A3 and =CE=A0 but no = Id) which models Type : Type. It is not trivial, but all types are inhabited (and have the fixed-point property). We can still interpret Girard's paradox in it, but it is not really a paradox without identity types as the type structure does not collapse. Has something like that known? (I fully expect Thomas to pull something out of his beard.) With kind regards, Andrej [For admin and other information see: http://www.mta.ca/~cat-dist/ ]