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