From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/7861 Path: news.gmane.org!not-for-mail From: Thomas Streicher Newsgroups: gmane.science.mathematics.categories Subject: Re: A category internal to itself Date: Fri, 6 Sep 2013 14:33:37 +0200 Message-ID: References: Reply-To: Thomas Streicher NNTP-Posting-Host: plane.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii X-Trace: ger.gmane.org 1378473368 27424 80.91.229.3 (6 Sep 2013 13:16:08 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Fri, 6 Sep 2013 13:16:08 +0000 (UTC) Cc: categories list To: Andrej Bauer Original-X-From: majordomo@mlist.mta.ca Fri Sep 06 15:16:07 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 1VHvtK-00086M-1d for gsmc-categories@m.gmane.org; Fri, 06 Sep 2013 15:16:02 +0200 Original-Received: from mlist.mta.ca ([138.73.1.63]:37774) by smtp3.mta.ca with esmtp (Exim 4.80) (envelope-from ) id 1VHvsK-0008UJ-D6; Fri, 06 Sep 2013 10:15:00 -0300 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1VHvsJ-0000yO-62 for categories-list@mlist.mta.ca; Fri, 06 Sep 2013 10:14:59 -0300 Content-Disposition: inline In-Reply-To: Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:7861 Archived-At: > The results would be a model of type theory (with ?? and ?? 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.) Indeed this was done in the Thesis of Nancy J. McCracken in 1979 supervised by John Reynolds. Its title is An investigation of programming languages with a polymorphic type structure. Cardelli and Wegner got interested in this in the mid 1980s. There are 2 paper on this one can find on the web Cardelli & Wegner On Understanding Types Data Abstraction and Polymorphism Computing Surveys, Vol.17 (1985) Cardelli A Polymorphic Lambda Calculus with Type:Type a DEC report from 1986 That's what I have wrung out of my beard Thomas [For admin and other information see: http://www.mta.ca/~cat-dist/ ]