If $f(x)=g(x)$ for all $x:A$, why is it not true that $\lambda x{.}f(x)=\lambda x{.}g(x)$?

Solution 1:

I’m pretty sure that the $\xi$ rule is implemented in Coq. The doc says somewhere

Let us write E[Γ] ⊢ t ▷ u for the contextual closure of the relation t reduces to u in the environment E and context Γ with one of the previous reduction β, ι, δ or ζ.

The $\xi$ rule is usually not even mentionned because this is a consequence of the contextual closure of definitional equality which is usually assumed.

In your concrete example, the problem does not come from $\xi$ but from the "fairly obvious" fact that $\langle\mathsf{proj_1}f(x),\mathsf{proj_2}f(x)\rangle=f(x)$. This is called $\eta$-equality for dependent sums, but Coq does not satisfy this definitionally (not even Coq 8.4 which has only $\eta$-equality for functions).

So yes, in Coq you have to prove $\eta$-equality for dependent sums using identity types, but this has nothing to do with $\xi$.

In Agda there is $\eta$-equality for dependent sums (and more generally for records), so probably that these two functions are definitionally inverse to each other in Agda.