# in the lambda calculus with products and sums is $f : [n] \to [n]$ $\beta\eta$ equivalent to $f^{n!}$?

$$\eta$$-reduction is often described as arising from the desire for functions which are point-wise equal to be syntactically equal. In a simply typed calculus with products it is sufficient, but when sums are involved I fail to see how to reduce point-wise equal functions to a common term.

For example, it is easy to verify that any function $$f: (1+1) \to (1+1)$$ is point-wise equal to $$\lambda x.f(fx)$$, or more generally $$f$$ is point-wise equal to $$f^{n!}$$ when $$f: A \to A$$ and $$A$$ has exactly $$n$$ inhabitants. Is it possible to reduce $$f^{n!}$$ to $$f$$? If not, is there an extension of the simply typed calculus which allows this reduction?

• What does "pointwise equal" mean, precisely? – Andrej Bauer Jan 9 at 22:35
• two functions $f, g:A \to A$ are point-wise equal if for any $a:A$, $f(a) =_{\beta\eta} g(a)$. – Jack Jan 10 at 20:20
• I am afraid this is not a sufficient explanation for type theory. What is $a$ here? Closed term? A term in a context? – Andrej Bauer Jan 11 at 7:53
• I would be happy to know a solution for closed terms. How about: two closed terms $f, g:A \to A$ are point-wise equal if for all closed terms $a:A, f(a) =_{\beta\eta} g(a)$? – Jack Jan 11 at 16:11
• Nope, you can't get that. – Andrej Bauer Jan 11 at 19:17