The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

Sorry for the confusion.

By Proof Irrelevance, I meant (the type of Coq.Logic.ProofIrrelevance.proof_irrelevance) :

forall (P : Prop) (p1 p2 : P), p1 = p2

By Function Extensionality, I meant (the type of Coq.Logic.FunctionalExtensionality.functional_extensionality_dep):

forall (A : Type) (B : A -> Type) (f g : forall x : A, B x), (forall x : A, f x = g x) -> f = g

= stands for Coq.Init.Logic.eq

Thanks for the responses, in particular, the reference to the CPP2017 paper, which I am reading right now.

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Tue, Dec 20, 2016 at 6:39 AM, Bas Spitters <b.a.w.spitters AT gmail.com> wrote:

You are right of course about UA. Although, one may consider the
question for Proof Irrelevance restricted to (h)Prop. I am not sure
which one Abhishek meant.

Proof Irrelevance restricted to hProp follows from UA.

On Tue, Dec 20, 2016 at 12:11 PM, Talia Ringer
<tringer AT cs.washington.edu> wrote:
> A friend recently made a pretty good argument that you can have predext
> without funext (which makes sense), so I think that would be the easiest
> metatheoretic way to show you can't prove proof irrelevance -> funext
> [predext -> propext -> proof irrelevance, so if proof irrelevance -> funext,
> then predext -> funext.] But I haven't actually formalized his argument yet,
> and it's 3 AM here so I likely won't get to think about this more tonight.
>
> The other direction strikes me as inherently not true otherwise UA would be
> inconsistent, but I also get really confused about how Prop interacts with
> univalent formalizations of Coq, so I could be off the mark.
>
> On Dec 20, 2016 2:30 AM, "Bas Spitters" <b.a.w.spitters AT gmail.com> wrote:
>
> Without really thinking about it, I guess the following techniques
> should work to show that neither is provable:
> http://www.pédrot.fr/articles/cpp2017.pdf
>
> On Tue, Dec 20, 2016 at 3:44 AM, Abhishek Anand
> <abhishek.anand.iitg AT gmail.com> wrote:
>> Without using any axiom, can one prove either of the following?
>>
>> 1) Proof Irrelevance -> Function Extensionality
>> 2) Function Extensionality -> Proof Irrelevance
>>
>> If not, is there a meta-theoretic argument about the unprovability of both
>> of them?
>>
>> Thanks,
>> -- Abhishek
>> http://www.cs.cornell.edu/~aa755/
>
>
>