coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] reasoning out of type equalities, Aleks Nanevski, 08/04/2012
- Message not available
- Re: [Coq-Club] reasoning out of type equalities, Kristopher Micinski, 08/04/2012
- Message not available
- Re: [Coq-Club] reasoning out of type equalities, Chung-Kil Hur, 08/04/2012
- Re: [Coq-Club] reasoning out of type equalities, Vladimir Voevodsky, 08/04/2012
- Re: [Coq-Club] reasoning out of type equalities, Aleksandar Nanevski, 08/05/2012
- Re: [Coq-Club] reasoning out of type equalities, andré hirschowitz, 08/05/2012
- Re: [Coq-Club] reasoning out of type equalities, Aleksandar Nanevski, 08/05/2012
- Re: [Coq-Club] reasoning out of type equalities, Vladimir Voevodsky, 08/05/2012
- Re: [Coq-Club] reasoning out of type equalities, Aleksandar Nanevski, 08/05/2012
- Re: [Coq-Club] reasoning out of type equalities, Vladimir Voevodsky, 08/05/2012
- Re: [Coq-Club] reasoning out of type equalities, Aleksandar Nanevski, 08/05/2012
- Re: [Coq-Club] reasoning out of type equalities, Adam Chlipala, 08/05/2012
- Re: [Coq-Club] reasoning out of type equalities, Aleksandar Nanevski, 08/05/2012
- Re: [Coq-Club] reasoning out of type equalities, andré hirschowitz, 08/05/2012
- Re: [Coq-Club] reasoning out of type equalities, Vladimir Voevodsky, 08/05/2012
- Re: [Coq-Club] reasoning out of type equalities, Aleksandar Nanevski, 08/05/2012
- Re: [Coq-Club] reasoning out of type equalities, Vladimir Voevodsky, 08/05/2012
- Re: [Coq-Club] reasoning out of type equalities, Aleksandar Nanevski, 08/05/2012
Archive powered by MHonArc 2.6.18.