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

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?

-
One small suggestion: this question seems like an excellent fit for the theoretical (or maybe non-theoretical?) CS SE sites, cstheory.stackexchange.com and cs.stackexchange.com; you might try migrating this question over there? –  Steven Stadnicki Jun 8 '12 at 16:52
@StevenStadnicki I didn't think of the CS SE, but maybe it's a good idea to migrate it. On the other hand, their lambda-calculus tag is not a lot bigger than the one here... –  Egbert Jun 8 '12 at 17:14
@StevenStadnicki it's worth pointing out that cstheory.SE is for research-level questions. –  user2468 Aug 6 '12 at 0:20

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.

-