# 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?