<p>The elimination rule states:</p>
<p><span class="math-container">$$
\frac{
\Gamma, x : 1 \vdash C : U_i \qquad
\Gamma \vdash c : C[\star/x] \qquad
\Gamma \vdash a : 1
}{
\Gamma \vdash \mathrm{ind}_1(x.C, c, a) : C[a/x]
}
$$</span>
You say that you want to &quot;just replace all the maps involving it with constant maps&quot;. First of all, not all terms involving the eliminator need be maps. For example, you could use <span class="math-container">$\mathrm{ind}_1$</span> to construct an element of <span class="math-container">$A \times B$</span>, so a pair.</p>
<p>What I think you have in mind is that you want to simply replace <span class="math-container">$\mathrm{ind}_1(x.C, c, a)$</span> with <span class="math-container">$c$</span>, is that it? You cannot do that, because <span class="math-container">$c$</span> has type <span class="math-container">$C[\star/x]$</span>, but <span class="math-container">$\mathrm{ind}_1(x.C, c, a)$</span> has type <span class="math-container">$C[a/x]$</span>. How do you know that <span class="math-container">$C[\star/x]$</span> and <span class="math-container">$C[a/x]$</span> are judgementally equal types? In fact, they need not be, since we do not have any rules that would allow us to conclude <span class="math-container">$\Gamma \vdash a \equiv_1 \star$</span>.</p>
<p>We could add such a rule, but that would change the nature of the unit type a bit, and it would also influence equality checking algorithms. But it can be done, in which case no eliminator is needed.</p>

CC BY-SA 4.0
2021-07-02T16:58:30.343Z
2021-07-02T17:34:02.227Z
2021-07-02T17:34:02.227Z
Andrej Bauer
<p>Example usage of <span class="math-container">$\top$</span>'s eliminator: to prove <span class="math-container">$\Pi_{x:\top} x=_1 \star$</span> (this is a propositional equality), the uniqueness principle of <span class="math-container">$\top$</span>.</p>
<p>With the eliminator, you can prove it by <em>eliminating</em> the parameter <span class="math-container">$x$</span>. This is a theorem that <em>must</em> take an instance of <span class="math-container">$\top$</span>. A constant map won't prove the theorem.</p>
<p>If you change the type checker to make it turn all instances of <span class="math-container">$\top$</span> into <span class="math-container">$\star$</span>, then the eliminator will be pointless. But this requires the normalization algorithm to be type-directed, while not all type theories are like this (a counterexample will be the Calculus of Constructions, the type theory of the Coq proof assistant).</p>

CC BY-SA 4.0
2021-07-03T11:21:37.850Z
Is $\equiv_1$ judgemental or propositional equality? And maybe write $\Pi$ instead of $\forall$, so emphasize we're in type theory (all sorts of people exist on the internet).
Andrej Bauer
CC BY-SA 4.0
2021-07-04T09:34:03.450Z
@AndrejBauer fixed
ice1000
CC BY-SA 4.0
2021-07-04T14:30:54.683Z
Ok, now I am using $\equiv$ for judgemental and you for propositional equality. We should try to make the notation consistent. I vote that you change yours :-) because the OP is referring to the HoTT book, which uses $=$ for propositional and $\equiv$ for judgemental equality.
Andrej Bauer
CC BY-SA 4.0
2021-07-04T15:20:50.887Z
@AndrejBauer makes sense :)
ice1000
CC BY-SA 4.0
2021-07-02T20:27:48.180Z
2021-07-04T15:20:23.777Z
2021-07-04T15:20:23.777Z
ice1000
<p>In the HoTT <a href="https://github.com/HoTT/book/wiki/Nightly-Builds" rel="nofollow noreferrer">book</a> p. 436 A.2.8 the eliminator <span class="math-container">$\mathrm{ind}_{\mathbf{1}}$</span> for the unit type is described.</p>
<p>What is the point of it? What if you did not introduce it and instead just replaced all the maps involving it with constant maps? That would not change much right?</p>

<type-theory>
What is the point of the eliminator for the unit type?
Rchjk
# What is the point of the eliminator for the unit type?

(Asked by: username_0 on 2021-07-02)

In the HoTT [book](https://github.com/HoTT/book/wiki/Nightly-Builds) p. 436 A.2.8 the eliminator $\mathrm{ind}\_{\mathbf{1}}$ for the unit type is described.

What is the point of it? What if you did not introduce it and instead just replaced all the maps involving it with constant maps? That would not change much right?

**Tags:** type-theory


---

## 2 answers

### Answer by username_1 on 2021-07-02. Score: 2

The elimination rule states:

$$
\frac{
\Gamma, x : 1 \vdash C : U\_i \qquad
\Gamma \vdash c : C[\star/x] \qquad
\Gamma \vdash a : 1
}{
\Gamma \vdash \mathrm{ind}\_1(x.C, c, a) : C[a/x]
}
$$
You say that you want to "just replace all the maps involving it with constant maps". First of all, not all terms involving the eliminator need be maps. For example, you could use $\mathrm{ind}\_1$ to construct an element of $A \times B$, so a pair.

What I think you have in mind is that you want to simply replace $\mathrm{ind}\_1(x.C, c, a)$ with $c$, is that it? You cannot do that, because $c$ has type $C[\star/x]$, but $\mathrm{ind}\_1(x.C, c, a)$ has type $C[a/x]$. How do you know that $C[\star/x]$ and $C[a/x]$ are judgementally equal types? In fact, they need not be, since we do not have any rules that would allow us to conclude $\Gamma \vdash a \equiv\_1 \star$.

We could add such a rule, but that would change the nature of the unit type a bit, and it would also influence equality checking algorithms. But it can be done, in which case no eliminator is needed.


---

### Answer by username_2 on 2021-07-02. Score: 2

Example usage of $\top$'s eliminator: to prove $\Pi\_{x:\top} x=\_1 \star$ (this is a propositional equality), the uniqueness principle of $\top$.

With the eliminator, you can prove it by *eliminating* the parameter $x$. This is a theorem that *must* take an instance of $\top$. A constant map won't prove the theorem.

If you change the type checker to make it turn all instances of $\top$ into $\star$, then the eliminator will be pointless. But this requires the normalization algorithm to be type-directed, while not all type theories are like this (a counterexample will be the Calculus of Constructions, the type theory of the Coq proof assistant).

> **Comments:**
> **username_1**: Is $\equiv_1$ judgemental or propositional equality? And maybe write $\Pi$ instead of $\forall$, so emphasize we're in type theory (all sorts of people exist on the internet).  
> **username_2**: @AndrejBauer fixed  
> **username_1**: Ok, now I am using $\equiv$ for judgemental and you for propositional equality. We should try to make the notation consistent. I vote that you change yours :-) because the OP is referring to the HoTT book, which uses $=$ for propositional and $\equiv$ for judgemental equality.  
> **username_2**: @AndrejBauer makes sense :)  

---

