<p>Yes, <span class="math-container">$\eta$</span> <em>reduction</em> for unit is terribly behaved. Suppose you are in a context <span class="math-container">$\Gamma \triangleq x:1, y:1$</span>.</p>
<p>Then, the unit term <span class="math-container">$\Gamma \vdash \left\langle\right\rangle : 1$</span> has the following eta-reductions:</p>
<p><span class="math-container">$$
\begin{array}{lcl}
\left\langle\right\rangle &amp; \leadsto_\eta &amp; x \\
\left\langle\right\rangle &amp; \leadsto_\eta &amp; y \\
\end{array}
$$</span></p>
<p>There are no further <span class="math-container">$\beta$</span> or <span class="math-container">$\eta$</span> reductions, so local confluence fails.</p>
<p>In practice (and in theory, actually), what you want to do instead is <span class="math-container">$\eta$</span>-<strong>expansion</strong>. You have to do it in a typed way, but it is fantastically well-behaved.</p>

CC BY-SA 4.0
2021-07-01T08:05:19.293Z
Or stop using $\eta$-rules and use an extensionality rule instead.
Andrej Bauer
CC BY-SA 4.0
2021-07-01T10:13:55.867Z
What do you mean by an extensionality rule?
Neel Krishnaswami
CC BY-SA 4.0
2021-07-01T10:20:51.117Z
See [Definition 3.22](https://arxiv.org/abs/2103.07397), 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.
Andrej Bauer
CC BY-SA 4.0
2021-06-30T11:05:21.737Z
2021-07-01T10:14:34.877Z
2021-07-01T10:14:34.877Z
Neel Krishnaswami
<p><a href="https://www.cse.chalmers.se/%7Eabela/lfsigma.pdf" rel="noreferrer">This paper</a> says: &quot;In the presence of a unit type, <span class="math-container">$\eta$</span>-reduction is not even locally confluent on well-typed terms [20].&quot;</p>
<p>[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 <span class="math-container">$\eta$</span>-reduction not being locally confluent on well-typed terms?</p>

CC BY-SA 4.0
2021-06-30T09:35:28.317Z
Where did you find the book? I didn't find an online version.
ice1000
<type-theory><lambda-calculus>
$\eta$-reduction not locally confluent on well-typed terms
capor
# $\eta$-reduction not locally confluent on well-typed terms

(Asked by: username_0 on 2021-06-30)

[This paper](https://www.cse.chalmers.se/%7Eabela/lfsigma.pdf) 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?

**Tags:** type-theory, lambda-calculus

> **Comments:**
> **username_1**: Where did you find the book? I didn't find an online version.  

---

## 1 answers

### Answer by username_2 on 2021-06-30. Score: 11

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.

> **Comments:**
> **username_3**: Or stop using $\eta$-rules and use an extensionality rule instead.  
> **username_2**: What do you mean by an extensionality rule?  
> **username_3**: See [Definition 3.22](https://arxiv.org/abs/2103.07397), 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.  

---

