From mboxrd@z Thu Jan 1 00:00:00 1970
X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/3042
Path: news.gmane.org!not-for-mail
From: Paul B Levy
Newsgroups: gmane.science.mathematics.categories
Subject: Re: Voevodsky on the homotopy lambda calculus
Date: Sun, 26 Feb 2006 12:38:27 +0000 (GMT)
Message-ID:
References:
NNTP-Posting-Host: main.gmane.org
Mime-Version: 1.0
Content-Type: TEXT/PLAIN; charset=US-ASCII
X-Trace: ger.gmane.org 1241019061 7003 80.91.229.2 (29 Apr 2009 15:31:01 GMT)
X-Complaints-To: usenet@ger.gmane.org
NNTP-Posting-Date: Wed, 29 Apr 2009 15:31:01 +0000 (UTC)
To: categories
Original-X-From: rrosebru@mta.ca Sun Feb 26 11:27:27 2006 -0400
Return-path:
Envelope-to: categories-list@mta.ca
Delivery-date: Sun, 26 Feb 2006 11:27:27 -0400
Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.52)
id 1FDNe6-0006yK-RX
for categories-list@mta.ca; Sun, 26 Feb 2006 11:17:14 -0400
In-Reply-To:
Original-Sender: cat-dist@mta.ca
Precedence: bulk
X-Keywords:
X-UID: 25
Original-Lines: 26
Xref: news.gmane.org gmane.science.mathematics.categories:3042
Archived-At:
> Phil Scott has been teaching me about the lambda calculus
> and related stuff. He noted that in getting a cartesian
> closed category from intuitionistic logic,
At the risk of boring people by repeating a point I've made on this list
before:
a model of intuitionistic logic is a *bi*cartesian closed category.
I see no reason to regard disjunction as more "peripheral" to
intuitionistic logic than implication. (And, likewise, no reason to
regard sum types as more peripheral to simple type theory than function
types.) Does anybody disagree?
Ccc's without coproducts (e.g. domains and continuous maps) arise in the
study of call-by-name languages with effects (e.g. divergence). But they
are not models of intuitionistic logic.
I appreciate that all John said was that a model constructed from syntax
is a ccc, which is true because it's a bi-ccc, so he didn't actually
contradict this point.
Paul