# $\eta$-reduction not locally confluent on well-typed terms

This paper says: "In the presence of a unit type, $$\eta$$-reduction is not even locally confluent on well-typed terms [20]."

[20] is a reference to a 300-page book with no further details and I cannot find the relevant example there. So can you give an example of $$\eta$$-reduction not being locally confluent on well-typed terms?

• Where did you find the book? I didn't find an online version. Commented Jun 30, 2021 at 9:35

Yes, $$\eta$$ reduction for unit is terribly behaved. Suppose you are in a context $$\Gamma \triangleq x:1, y:1$$.

Then, the unit term $$\Gamma \vdash \left\langle\right\rangle : 1$$ has the following eta-reductions:

$$\begin{array}{lcl} \left\langle\right\rangle & \leadsto_\eta & x \\ \left\langle\right\rangle & \leadsto_\eta & y \\ \end{array}$$

There are no further $$\beta$$ or $$\eta$$ reductions, so local confluence fails.

In practice (and in theory, actually), what you want to do instead is $$\eta$$-expansion. You have to do it in a typed way, but it is fantastically well-behaved.

• Or stop using $\eta$-rules and use an extensionality rule instead. Commented Jul 1, 2021 at 8:05
• What do you mean by an extensionality rule? Commented Jul 1, 2021 at 10:13
• See Definition 3.22, for the unit type it is $$\frac{\vdash a : 1 \qquad \vdash b : 1}{\vdash a \equiv_1 b}$$ and examples are on the next page. Commented Jul 1, 2021 at 10:20