coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club]a type equality question

From: Benjamin Werner <benjamin.werner AT inria.fr>
To: Vladimir Voevodsky <vladimir AT ias.edu>
Cc: Coq Club <coq-club AT pauillac.inria.fr>
Subject: Re: [Coq-Club]a type equality question
Date: Thu, 25 May 2006 02:09:56 +0200
Domainkey-signature: a=rsa-sha1; q=dns; c=nofws; s=beta; d=gmail.com; h=received:in-reply-to:references:mime-version:content-type:message-id:cc:content-transfer-encoding:subject:date:to:x-mailer:from:sender; b=eYDkIksC8L4KCEEA1D1YPz4bb3D7hQ0GAG8r4Crw/Kffn1lQ43XlJUMruiM2xX2BmIXb43gqXJxO7CJFnxSPQxnJVKT+WqGElDKr4olJTvNdeeV+MJ6OLXn2f0WOIWT609zeFyRXc72mmH2g+MdMQWEUt8VX60jvWnUNmiQkMqg=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

It is a late and short answer, but my strong guess would be

2 is not provable; it is not verified by simple set-theoretic semantics

1 is seems not provable; but I am not sure what a model looks like which
verifies 2 (that is falsifies 1)

cheers,

Benjamin

Le 14 avr. 06 � 19:06, Vladimir Voevodsky a �crit :

Are any one of the following two opposite statements provable in Coq (with or without the boolean assumption):

1. there exist types A, B, C such that A->(B->C) is not equal to B-> (A->C)
2. for all A, B, C one has A->(B->C) = B->(A->C)

If neither one is provable can one prove (outside of coq) that both are not provable?

Vladimir.

--------------------------------------------------------
Bug reports: http://coq.inria.fr/bin/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

Re: [Coq-Club]a type equality question, Benjamin Werner