coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Vladimir Voevodsky <vladimir AT ias.edu>
- To: Aleksandar Nanevski <aleks.nanevski AT imdea.org>
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] reasoning out of type equalities
- Date: Sun, 5 Aug 2012 12:13:46 -0400
- Envelope-to: aleks.nanevski AT imdea.org, coq-club AT inria.fr
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)))
- [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, Vladimir Voevodsky, 08/06/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.