The Coq mailing list

[Talia Ringer <tringer AT cs.washington.edu>]

I guess more simply you could skip thinking about predext altogether and just consider propext.

On Dec 20, 2016 3:11 AM, "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/