Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] reasoning out of type equalities

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] reasoning out of type equalities


Chronological Thread 
  • From: Vladimir Voevodsky <vladimir AT ias.edu>
  • To: "Aleks Nanevski" <aleks.nanevski AT imdea.org>
  • Cc: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] reasoning out of type equalities
  • Date: Sat, 4 Aug 2012 16:40:46 -0400
  • Envelope-to: aleks.nanevski AT imdea.org, coq-club AT inria.fr

This is not provable. In fact in combination with propositional
extensionality (axiom saying that for A,B:Prop one has (A<->B)->(A=B ) it
would imply the excluded middle.

Indeed, for all A:Prop, (A or (not A) is nonempty and on the other hand

((A or (not A)) and True) <-> (A or (not A) ) <-> ((A or (not A)) and (A
or (not A)))

V.


On Aug 4, 2012, at 1:19 PM, Aleks Nanevski wrote:

> Hi,
>
> Given a nonempty type B, I was wondering if the following is provable:
>
> forall A1 A2 : Type, A1 * B = A2 * B -> A1 = A2
>
> Thanks,
> Aleks




Archive powered by MHonArc 2.6.18.

Top of Page