$ \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?