2
$\begingroup$

In the HoTT book 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?

$\endgroup$
2
$\begingroup$

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.

$\endgroup$
2
$\begingroup$

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).

$\endgroup$
4
  • $\begingroup$ 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). $\endgroup$ Jul 3 at 11:21
  • $\begingroup$ @AndrejBauer fixed $\endgroup$
    – ice1000
    Jul 4 at 9:34
  • 1
    $\begingroup$ 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. $\endgroup$ Jul 4 at 14:30
  • $\begingroup$ @AndrejBauer makes sense :) $\endgroup$
    – ice1000
    Jul 4 at 15:20

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.