The Coq mailing list

[Aleksandar Nanevski <aleks.nanevski AT imdea.org>]

Ok. Thanks for the answer.

-Aleks

On 8/4/12 10:40 PM, Vladimir Voevodsky wrote:
> 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