coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Théo Zimmermann <theo.zimmi AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Impredicative set + function extensionality + proof irrelevance consistent?
Date: Wed, 21 Dec 2016 14:33:10 +0000
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=theo.zimmi AT gmail.com; spf=Pass smtp.mailfrom=theo.zimmi AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm0-f50.google.com
Ironport-phdr: 9a23:JVSQiRB1vOSGYDAJgEz7UyQJP3N1i/DPJgcQr6AfoPdwSPv+rsbcNUDSrc9gkEXOFd2CrakV0KyG6eu9ACQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9GiTe5b75+Nha7oRveusQWnIdpN7o8xAbOrnZUYepd2HlmJUiUnxby58ew+IBs/iFNsP8/9MBOTLv3cb0gQbNXEDopPWY15Nb2tRbYVguA+mEcUmQNnRVWBQXO8Qz3UY3wsiv+sep9xTWaMMjrRr06RTiu86FmQwLuhSwaNTA27XvXh9R/g6JVoh2vpxJxzY3Jbo+LKPVzZbnScc8ASGdbQspdSy5MD4WhZIUPFeoBOuNYopHjqVsOtxy+AhGjC+Duyj9Ng3/5w7c60+E7HgHA2gwrAtUDsGjUrNrrM6ceS+G0zKjNzTXGbvNbwjj96I3SfRAgpfGAR65/cc3UyUQ2EQ7Ok1ueqYvgPzyP1+QNtXCW7/F8Ve21l2EnqAZxoiaxycc2hInJgoUVy17e+Splx4Y1INu1Q1N4b968CJZdtS6XO5FrTs88Q2xkoiU3xqMctZO7YCQHzoksyQTFZPydaYeI5wruVOaPLjd8g3JoYLe/iAyz8Uik0+H9WMy03EpToipLktTAqmoB1xPU6siARft9+lmu1SyT2ADU7+FIOUE0lazFJJ492rM9lJUevV7eEiPomEj6lqybels+9uWo9+jrerDmqYWdN49whAH+KKMumsmnDOQkMggBQW+b9f691b3i+E35RbRKg+Y5kqncqp/aJMAbqrSlDA9S14Yv8wy/ACu+0NQEgXkHK0pIdw6Aj4jwIl3BPPT4DeqkjFm3izdqx/XGPqX7DZnXL3jDlq3hfbdn5EJGxgoz14MX25UBAbYYZfn3R0XZtdrCDxZ/PRbn7fzgDYBB1gIZblCOB6qUKqbbt1nAsv4vLu7Kdo4QvTfVJP0s5vqohng8zwxONZK11IcaPSjrVs9tJF+UNCLh

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

[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