There's something about lambda calculus that keeps me puzzled. Suppose we have $x:A\vdash f(x):P(x)$ and $x:A\vdash g(x):P(x)$ for some dependent type $P$ over a type $A$. Then it is not necessarily true that $\lambda x{.}f(x)=\lambda x{.}g(x)$.
I've tried to understand this phenomenon and then it goes something like this: actually, the argument you pass to $\lambda$ is not just $x{.}f(x)$, but it is the entailment $x:A\vdash f(x):P(x)$. Thus different reasons why $f(x):P(x)$ for each $x:A$ give different functions. But I've never seen things like this written down somewhere, so I feel quite uncertain about it.
I'd like to know why $\lambda x{.}f(x)$ is not $\lambda x{.}g(x)$ even if $f(x)=g(x)$. From a type theoretical point of view, but maybe also from a models point of view. If there are models that can easily explain what kind of behavior we can expect from $\lambda$, that would be very helpful.
Edit. I should add that the bit of lambda calculus I have learned is from doing dependent type theory (and more specifically, Martin-Lof's intensional type theory) in Coq. There, the dependent product $$\prod(x:A),\ P(x)$$ is defined for a dependent type $P:A\to\mathsf{Type}$ over a type $A$ by introducing elements $\lambda x{.}f(x)$ for each $x:A\vdash f(x):P(x)$, with for each $f:\prod(x:A),\ P(x)$ and each $a:A$, a term $\mathsf{apply}(f,a):P(a)$. These are then required to satisfy the $\beta$- and $\eta$-conversion rules:
$$
\begin{split}
\beta.\qquad\qquad & \mathsf{apply}(\lambda x{.}f(x), a)=f(a)\\
\eta.\qquad\qquad & \lambda x{.}\mathsf{apply}(f,x)=f,
\end{split}
$$
but not rule $\xi$, which is the rule saying that $\lambda x{.}f(x)=\lambda x.g(x)$ whenever $f(x)=g(x)$ for all $x:A$. But I don't know about anything that would break rule $\xi$, hence my question.
Here's a concrete example where I face this problem.
An example of such $f$ and $g$ where this problem bugged me the most comes from proving that the axiom of choice is an equivalence. Suppose that $A$ is a type, that $P$ is a dependent type over $A$ and that $R$ is a dependent type over $P$, i.e. $R:\prod(x:A),\ (P(x)\to\mathsf{Type})$. Then the type theoretical axiom of choice is the function
$$
\mathsf{ac}:\prod(x:A)\sum (u:P(x)),\ R(x,u)\to\sum\Big(s:\prod(x:A),\ P(x)\Big)\prod(x:A),\ R(x,s(x))
$$
given by
$$
\lambda f.\langle \lambda x.\mathsf{proj_1}f(x),\lambda x.\mathsf{proj_2}f(x)\rangle
$$
A candidate inverse would be given by
$$
\mathsf{ac{-}inv}:=\lambda w.\lambda x.\langle\mathsf{proj_1}w(x),\mathsf{proj_2}w(x)\rangle.
$$
To prove that this is a right inverse you need the $\eta$-conversion at some point, but to prove that it is a left inverse, the identity
$$
\lambda x.\langle\mathsf{proj_1}f(x),\mathsf{proj_2}f(x)\rangle=\lambda x.f(x)
$$
is needed at some point. While it is fairly obvious that $\langle\mathsf{proj_1}f(x),\mathsf{proj_2}f(x)\rangle=f(x)$ for each $x:A$, this is not a step you can make in Coq, because there's no rule $\xi$ there (as far as I know). Even $\eta$ you have to introduce manually and that is only possible using the identity types of Martin-Lof. Mike Shulmann has constructed a way around this issue: there is a proof that the map $\mathsf{ac}$ is indeed an equivalence. I understand this proof, but not the behavior of $\lambda$. What can $\lambda$ do if you don't have $\xi$ that prohibits me from making this step?
Best Answer
I’m pretty sure that the $\xi$ rule is implemented in Coq. The doc says somewhere
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.