30

The Coq FAQ says that function extensionality is consistent with predicative Set. It's not fully clear to me from this whether it's consistent with impredicative Set (or maybe the consistency is unknown in that case).

András Kovács
  • 29,931
  • 3
  • 53
  • 99
  • 2
    This sounds a bit misleading; I imagine that it is consistent with impredicative Set as well. But that's probably a better question for the Coq mailing list. – Arthur Azevedo De Amorim Nov 03 '16 at 07:49
  • 1
    Additionally, this question is about the theory of Coq rather than a programming issue with Coq and should probably be migrated to MathOverflow where it has more chances of being answered in details. – Zimm i48 Nov 03 '16 at 10:53
  • 2
    If you're considering migration then [cstheory.SE](http://cstheory.stackexchange.com) would be another good choice, imo. – Anton Trunov Nov 03 '16 at 15:47
  • This question has been mentioned by [Zimm i48](http://stackoverflow.com/users/3335288/zimm-i48) in [this](https://sympa.inria.fr/sympa/arc/coq-club/2016-12/msg00114.html) related Coq-Club thread ([this](https://sympa.inria.fr/sympa/arc/coq-club/2016-12/msg00115.html) post specifically). – Anton Trunov Dec 21 '16 at 14:39

0 Answers0