[Coq-Club] function extensionality with finite domains

[Abhishek Anand]

Is the following provable:
Lemma fextb: forall (f g: bool -> bool) (p: forall b, f b = g b), f =g.

For CoC, the following paper (Definition 2) gives a countermodel:
Boulier, Simon, Pierre-Marie Pédrot, and Nicolas Tabareau. “The Next 700
Syntactical Models of Type Theory.” In CPP. Paris, 2017.
https://www.pédrot.fr/articles/cpp2017.pdf
<https://www.xn--pdrot-bsa.fr/articles/cpp2017.pdf>.

Can this countermodel scale up to Coq?

[Pierre-Marie Pédrot]

Lemma fextb: forall  (f g: bool -> bool) (p: forall b, f b = g b), f =g.
Boulier, Simon, Pierre-Marie Pédrot, and Nicolas Tabareau. “The Next 700
Syntactical Models of Type Theory.” In CPP. Paris, 2017.
https://www.pédrot.fr/articles/cpp2017.pdf
<https://www.xn--pdrot-bsa.fr/articles/cpp2017.pdf>.
Can this countermodel scale up to Coq?

Define precisely "Coq".

(Protip: nobody knows, and it is a moving target anyways.)

The only limitation of this model is that it doesn't satisfy
eta-expansion, but it can pretty much accomodate any other feature of Coq.

If you want to negate funext and still have eta, you can have a look at
the exceptional model: https://hal.inria.fr/hal-01840643. That one has
another limitation, namely that there is no singleton elimination from
Prop to Type (you can only eliminate empty types).

PMP