The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

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