From mboxrd@z Thu Jan  1 00:00:00 1970
X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/2346
Path: news.gmane.org!not-for-mail
From: Paul B Levy <P.B.Levy@cs.bham.ac.uk>
Newsgroups: gmane.science.mathematics.categories
Subject: Re: topos logic arising nicely
Date: Mon, 9 Jun 2003 10:18:11 +0100 (BST)
Message-ID: <Pine.LNX.4.44.0306091006420.7512-100000@acws-0092.cs.bham.ac.uk>
References: <200306051946.VAA19086@fb04305.mathematik.tu-darmstadt.de>
NNTP-Posting-Host: main.gmane.org
Mime-Version: 1.0
Content-Type: TEXT/PLAIN; charset=US-ASCII
X-Trace: ger.gmane.org 1241018594 3697 80.91.229.2 (29 Apr 2009 15:23:14 GMT)
X-Complaints-To: usenet@ger.gmane.org
NNTP-Posting-Date: Wed, 29 Apr 2009 15:23:14 +0000 (UTC)
To: categories@mta.ca
Original-X-From: rrosebru@mta.ca Mon Jun  9 11:50:19 2003 -0300
Return-path: <cat-dist@mta.ca>
Envelope-to: categories-list@mta.ca
Delivery-date: Mon, 09 Jun 2003 11:50:19 -0300
Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.10)
	id 19PNwj-0003Ns-00
	for categories-list@mta.ca; Mon, 09 Jun 2003 11:48:29 -0300
In-Reply-To: <200306051946.VAA19086@fb04305.mathematik.tu-darmstadt.de>
Original-Sender: cat-dist@mta.ca
Precedence: bulk
X-Keywords: 
X-UID: 37
Original-Lines: 22
Xref: news.gmane.org gmane.science.mathematics.categories:2346
Archived-At: <http://permalink.gmane.org/gmane.science.mathematics.categories/2346>

On Thu, 5 Jun 2003, Thomas Streicher wrote:

> Hi Paul,
>
> > "The neglect of sum types is the root of all evil."
>
> To some extent this may be true for programming languages (but see recent
> work of Jim Laird). For logics it is less clear. Actually you mean the
> empty type, isn't it?

which is the n=0 instance of the n-ary sum connective.  So it should be
included in even the simply typed setting.

Paul

> Moreover, sunset types are slightly heavier than
> ordinary sum types. Subset types are rather dependent sum types.