The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

I believe UA at universe i implies funext at universe i (but *not* at universes j > i), and UA (funext) at universe i implies UA (respectively, funext) at universes j < i, but *not* universes j > i.  Proof irrelevance + propext gives you UA for Prop.  Unless impredicativity is doing something strange, this shouldn't give you funext at any universes above Prop.

Indeed, if FE -> PI, then UA is inconsistent, since UA implies both FE and not PI.

Bas, isn't proof irrelevance for hProps just the definition of an hProp?  (Are you thinking of propext?)

On Tue, Dec 20, 2016, 10:51 AM Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

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/
>
>
>