The Coq mailing list

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

I see. Ok, thanks for the detailed answer.

Indeed, it's that last case:

forall (A1 A2 B : Type), B -> (A1*B = A2*B) -> (A1=A2)

with equality in Prop, that applies to my problem.

It's amusing that I've ran into univalence just by trying to hack up a bit of meta theory for concurrency. I guess I'll now have to read up on it.

Best,
Aleks

On 8/5/12 6:13 PM, Vladimir Voevodsky wrote:

Here are some further cases:

Under the assumption (exists v:B, True) it becomes dependent on how you define = . If = lives in Prop then it is provable at least as a corollary of the univalence axiom (which is a generalization of propositional extensionality). 

If = lives in Type then it is not provable.  The argument for this is a bit more complex. Note first that if it were provable in the empty context then it would be provable in any context G. In the univalent model it would mean that for any fibration p:B -> G such that "(exists v:B, True)" i.e. such that  p is surjective and any A1 -> G, A2 -> G a weak equivalence between A1 x_G B and A2 x_G B over G gives a weak equivalence between   A1 and A2 over G. This is not true. For example one can take G to have a non-trivial fundamental group pi_1, B to be the universal covering of G and A1 and A2 to be any two non-isomorphic unramified coverings of G of the same degree.  

This example by the way also shows that in case when = lives in Type your statement for B such that (exists v:B, True) does not follow from the axiom of the excluded middle which is satisfied by the UA. 

Finally, if you assume an actual term of type B then your statement becomes a provable corollary of the univalent axiom. I.e. the following is provable modulo UA:

forall (A1 A2 B : Type), B -> (A1*B = A2*B) -> (A1=A2)

where = can now be either in Prop or in Type.  

V. 

On Aug 5, 2012, at 8:45 AM, Aleksandar Nanevski wrote:

Interesting.

Ok, what if nonempty B is defined as (exists v : B, True), rather than as (B <> False)?

-Aleks

On 8/5/12 2:20 PM, Vladimir Voevodsky wrote:

No. 

not((A or (not A)) = False) <-> not(not(A or (not A)) <->  not ((not A) and A) <-> not(False) <-> True.

V.

On Aug 5, 2012, at 7:48 AM, Aleksandar Nanevski wrote:

Is False supposed to be the type B that gets cancelled in my example

  A1 * B = A2 * B -> A1 = A2?

If so, then I'm not sure your argument applies. I have postulated that B is nonempty, and hence can't be False.

I now realize that the same issue appears in Vladimir's email: If B = (A or not A) is nonempty, then isn't excluded middle already assumed?

-Aleks

On 8/5/12 12:53 PM, andré hirschowitz wrote:

This could probably be simplified into

False * True <-> False <-> False * False.

ah 

2012/8/4 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)))