The Coq mailing list

[roux cody <cody.roux AT gmail.com>]

As a side note, http://cstheory.stackexchange.com is a really appropriate place for these kinds of questions, and Coq-theory/CIC questions would really be appreciated there!

On Wed, Dec 21, 2016 at 9:33 AM, Théo Zimmermann <theo.zimmi AT gmail.com> wrote:

This is a question that came up a short while ago on Stack Overflow as well: http://stackoverflow.com/questions/40395946/compatibility-of-impredicative-set-and-function-extensionality

I talked with Hugo about it who said that it probably is consistent but has not been proved so to his knowledge.

If someone has a better answer to that, please answer both here and there.

Théo

Le mer. 21 déc. 2016 à 11:36, Kristina Sojakova <sojakova.kristina AT gmail.com> a écrit :

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