Tag Info

Yes, this is provable—indeed, it is provable by reflexivity. This is because Coq has eta-equality of functions built into its notion of definitional equality. ...

As for your follow-up question: Coq implements η-conversion, but not η-reduction/expansion, because η really is treated at the level of the conversion test and not at that of reduction (which is a sub-...

Is the injectivity of 𝑇𝑇𝑜𝑏𝑠/𝐶𝐶𝑜𝑏𝑠 also anti-classical? It isn't. The setoid model in the TTobs paper supports LEM (meaning that every setoid is empty or nonempty). This note explains that ...

Kind of fun to note that extensionality is inconsistent with the internal Church Thesis which states that every function $\mathbb{N}\rightarrow\mathbb{N}$ is realized by some Turing machine. In turn ...

Function extensionality is “safe“ in the sense that it is valid in traditional constructive mathematics, for example as practiced by Erret Bishop, as well as in any topos. It is also valid in homotopy ...

To expand on @NaïmFavier's answer: The key here is the difference between definitional and propositional equality. Most times, when people talk about "function extensionality" they mean ...

The new rule seems to be equivalent to funext plus the definitional equality that says that funext of constant refl is refl. As ...

You don't need function extensionality to prove that, only the $\eta$-rule for functions: then both sides are equal to $\lambda x y.\ f x y$. I don't know if that's how Coq does it.