coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Impredicative set + function extensionality + proof irrelevance consistent?

From: Kristina Sojakova <sojakova.kristina AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Impredicative set + function extensionality + proof irrelevance consistent?
Date: Tue, 20 Dec 2016 19:32:19 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=sojakova.kristina AT gmail.com; spf=Pass smtp.mailfrom=sojakova.kristina AT gmail.com; spf=None smtp.helo=postmaster AT mail-yw0-f178.google.com
Ironport-phdr: 9a23:1auBUBSKB+7t5viArlBcNatGMNpsv+yvbD5Q0YIujvd0So/mwa67bBeN2/xhgRfzUJnB7Loc0qyN4vumCTRLu8jJ8ChbNscTB1ld0YRetjdjKfDGIHWzFOTtYS0+EZYKf35e1Fb/D3JoHt3jbUbZuHy44G1aMBz+MQ1oOra9QdaK3Izkn9y1rpbUekBDgCe3SbJ0NhS/6wvL5ecMho43Cbww0QfIpHIAQONUzGBvO1vbyw375M6z+4BqtSdKuuk99shJear/dqU8C7dfCWJ1YCgO+MT3uEybHkO07XwGXzBOnw==

Dear all,

As the subject suggests, I am using Coq with the -impredicative-set flag and importing modules FunctionalExtensionality and ProofIrrelevance (both in the subdirectory Logic). Is this theory known to be consistent?

I read the FAQ and there is no mention of it not being consistent but I would like to know for sure.

Thank you,

Kristina

[Coq-Club] Impredicative set + function extensionality + proof irrelevance consistent?, Kristina Sojakova, 12/21/2016
- Re: [Coq-Club] Impredicative set + function extensionality + proof irrelevance consistent?, Théo Zimmermann, 12/21/2016
  - Re: [Coq-Club] Impredicative set + function extensionality + proof irrelevance consistent?, roux cody, 12/21/2016