coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Aleksandar Nanevski <aleks.nanevski AT imdea.org>
- To: Vladimir Voevodsky <vladimir AT ias.edu>
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] reasoning out of type equalities
- Date: Sun, 05 Aug 2012 18:58:06 +0200
- Organization: IMDEA Software Institute
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:
|
- [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.