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
131 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 ...
Russoul's user avatar
  • 345
5 votes
1 answer
160 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 ...
Ilk's user avatar
  • 517
4 votes
0 answers
94 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 ...
Trebor's user avatar
  • 3,738
13 votes
2 answers
428 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 ...
Couchy's user avatar
  • 2,181