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.
4
questions
2
votes
1
answer
111
views
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 ...
- 345
5
votes
1
answer
139
views
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 ...
- 517
4
votes
0
answers
81
views
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 ...
- 3,678
13
votes
2
answers
325
views
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
...
- 2,141