coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Proof Irrelevance <-> Function Extensionality?

From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] Proof Irrelevance <-> Function Extensionality?
Date: Mon, 19 Dec 2016 21:44:35 -0500
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk0-f171.google.com
Ironport-phdr: 9a23:bMS6nxb1P7ioSSTG5JqSYtT/LSx+4OfEezUN459isYplN5qZr8y+bnLW6fgltlLVR4KTs6sC0LuN9f+wEjFYqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjSwbLd8IRmsrwjctcYajIt+Jq0s1hbHv3xEdvhMy2h1P1yThRH85smx/J5n7Stdvu8q+tBDX6vnYak2VKRUAzs6PW874s3rrgTDQhCU5nQASGUWkwFHDBbD4RrnQ5r+qCr6tu562CmHIc37SK0/VDq+46t3ThLjlSEKPCM7/m7KkMx9lKJVrhyiqRJi3YDbfJqYO+Bicq7HZ94WWXZNU8RXWidcAo28dYwPD+8ZMOtEtIb9p1oOrQC+BQayB+Pk1yNFhnns0q08zusqDAbL0xY7ENIOsXTUt9X1O7kRUeyv1qbIyy/Mb/VL1jvn6YjIcwwhof6XULJ/dMre00gvFwffglqMrozlOiqY2+IQuGaV6OpgUPigi28hqwxpvjevwd0sio/XiYIRzlDI7zt2z5soJdC+VUV1YsakHYNOuy2GM4Z6WMAvTmFytCok1LEKpYS3cDUIxZg6wRPUduaJfJKS4h35UeacOTd4i2xheLK4nxuy9FKvyuz4VsWtyVZKrTZJnsDCtnwQ1RHf99KLSvR6/kem1jaP0x7c5vtYLkAzkKrXM58hwrgumZoPqUnPADP6lUHsgKKVdkgo4Pak5/r7brn8u5ORNZJ4hhn7Mqs0m8y/Beo4MhIJX2ie4emzzqbs/U34QLVRjv05jKrZvIrAKsQdvKG5BRJa3pwi6xa+Ezem388VnXYCLF1feRKHi5LlNE3JIPD9Ffu/mUijkC93x/DaOb3sGonCLn/akLv4Ybl971NcxxEowNBE55NUD6kBL+jpVk/wstzYFB45PBauz+bpEtUunr8ZDGmIG+qSNL7Y+QuD4ftqKO2RbqcUviz8Ir4r/ai9o2U+nAo0d6moxpsaaziRGP1gLw3NaHDsg8wBHGRMtww3SuCsiVyeXhZcYn+zW+Q34TRtW9HuNpvKWo342O/J5yy8BJADPm0=

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/

[Coq-Club] Proof Irrelevance <-> Function Extensionality?, Abhishek Anand, 12/20/2016
- Re: [Coq-Club] Proof Irrelevance <-> Function Extensionality?, Bas Spitters, 12/20/2016
  - Re: [Coq-Club] Proof Irrelevance <-> Function Extensionality?, Talia Ringer, 12/20/2016
    - Re: [Coq-Club] Proof Irrelevance <-> Function Extensionality?, Talia Ringer, 12/20/2016
    - Re: [Coq-Club] Proof Irrelevance <-> Function Extensionality?, Bas Spitters, 12/20/2016
      - Re: [Coq-Club] Proof Irrelevance <-> Function Extensionality?, Abhishek Anand, 12/20/2016
        
        Re: [Coq-Club] Proof Irrelevance <-> Function Extensionality?, Jason Gross, 12/21/2016