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.
6
questions
1
vote
2
answers
243
views
Why did this proof succeed without function extensionality?
I'm very confused as to why a proof of a lemma succeeded without function extensionality.
I'm messing around with some trivial Coq proofs for manipulating pseudosequences of the form ...
- 3,073
3
votes
2
answers
229
views
Has extensionality ever caused any problems in a mathematical proof?
I read the following about extensionality in PLFA,
Agda does not presume extensionality, but we can postulate that it
holds:
...
- 2,210
2
votes
1
answer
141
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
176
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 ...
- 547
4
votes
0
answers
106
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 ...
- 4,025
13
votes
2
answers
486
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,290