Questions tagged [functional-extensionality]

Use this tag for the principle of functional extensionality in logic and proofs which states that two functions are equal if their values are equal at every argument.

Filter by
Sorted by
Tagged with
2 votes
1 answer

Provable `fun-ext`and "rewriting under binders" in intensional MLTT

I've noticed that the underlying judgemental machinery of intensional MLTT can be extended such that function extensionality becomes provable. Or in other words it becomes possible to "rewrite ...
Russoul's user avatar
  • 345
5 votes
1 answer

State of art for observational equality, on the injectivity requirement

I am reading through the papers, "Observational equality: Now for good" (${TT}^{obs}$) and "Impredicative Observational Equality" (${CC}^{obs}$) by Pujet and Tabareau, and I am ...
Ilk's user avatar
  • 517
4 votes
0 answers

Independence of function extensionality

Who first realized that function extensionality cannot be proved within vanilla MLTT, or some variations of it? Now to my knowledge the simplest way to show this is by syntactic models. But surely ...
Trebor's user avatar
  • 3,738
13 votes
2 answers

Is eta-equality provable in Coq?

Trying to answer another question, I can't help second guessing myself about whether eta equality is provable in Coq. In particular, can one prove ...
Couchy's user avatar
  • 2,181