[proofplan]
The eliminator is the non-dependent recursor for the unit type: to define a function out of $\top$, it is enough to specify the image of its constructor $\ttstar$. The computation rule is exactly the beta rule for this recursor. For uniqueness, we compare an arbitrary function $f : \top \to C$ with the recursor determined by $f(\ttstar)$ pointwise; propositional eta for $\top$ reduces every input $x : \top$ to $\ttstar$, and function extensionality turns the resulting pointwise identity into an identity of functions. The final judgmental clause is separate: it is a statement about definitional equality in a stronger judgmental theory, not a constructed path.
[/proofplan]
[step:Construct the recursor from the value at $\ttstar$]
Fix a term $c : C$. By the elimination rule for the unit type, the datum of the value $c : C$ at the constructor $\ttstar : \top$ determines a function
\begin{align*}
\operatorname{rec}_{\top}(c) : \top \to C.
\end{align*}
Its defining beta computation rule gives
\begin{align*}
\operatorname{rec}_{\top}(c)(\ttstar) = c.
\end{align*}
This proves the asserted existence of the eliminator and its computation rule.
[/step]
[step:Reduce uniqueness to pointwise equality on $\top$]
Let
\begin{align*}
f : \top \to C
\end{align*}
be any function, and define
\begin{align*}
r : \top \to C
\end{align*}
by
\begin{align*}
r := \operatorname{rec}_{\top}(f(\ttstar)).
\end{align*}
As declared in the statement, $\operatorname{Id}_A(a,b)$ denotes the identity type of two terms $a,b : A$, and $a =_A b$ is the same identity type notation. We will construct a dependent function
\begin{align*}
h : \prod_{x : \top} \operatorname{Id}_C(f(x),r(x)).
\end{align*}
Fix $x : \top$. By the assumed propositional eta principle for $\top$, there is a path
\begin{align*}
\eta_{\top}(x) : \operatorname{Id}_{\top}(x,\ttstar).
\end{align*}
We prove $\operatorname{Id}_C(f(x),r(x))$ by path induction on $\eta_{\top}(x)$. In the reflexivity case, $x$ is $\ttstar$, so the required type is
\begin{align*}
\operatorname{Id}_C(f(\ttstar),r(\ttstar)).
\end{align*}
By the computation rule for $r = \operatorname{rec}_{\top}(f(\ttstar))$, there is a path
\begin{align*}
r(\ttstar) = f(\ttstar).
\end{align*}
Taking its inverse gives
\begin{align*}
f(\ttstar) = r(\ttstar).
\end{align*}
Thus path induction supplies the required term $h(x)$ for every $x : \top$.
[guided]
We want to prove that $f$ and $r$ are the same function. In an intensional [type theory](/page/Type%20Theory), equality of functions is not obtained merely by saying that $\top$ has one element; we first build pointwise equality.
Let
\begin{align*}
f : \top \to C
\end{align*}
be fixed, and define the comparison function
\begin{align*}
r : \top \to C
\end{align*}
by
\begin{align*}
r := \operatorname{rec}_{\top}(f(\ttstar)).
\end{align*}
Here $\operatorname{Id}_A(a,b)$ denotes the identity type of two terms $a,b : A$, as fixed in the theorem statement. The goal is to construct
\begin{align*}
h : \prod_{x : \top} \operatorname{Id}_C(f(x),r(x)).
\end{align*}
Now fix an input $x : \top$. The propositional eta principle for the unit type gives a path
\begin{align*}
\eta_{\top}(x) : \operatorname{Id}_{\top}(x,\ttstar).
\end{align*}
This path is the formal replacement for the informal statement that every element of $\top$ is the constructor $\ttstar$. We use path induction on $\eta_{\top}(x)$ with the family of goals
\begin{align*}
\operatorname{Id}_C(f(x),r(x)).
\end{align*}
Path induction reduces the problem to the reflexivity case $x \equiv \ttstar$. In that case the required identity is
\begin{align*}
\operatorname{Id}_C(f(\ttstar),r(\ttstar)).
\end{align*}
By the beta computation rule for the unit recursor applied to the chosen value $f(\ttstar) : C$, we have
\begin{align*}
r(\ttstar) = \operatorname{rec}_{\top}(f(\ttstar))(\ttstar) = f(\ttstar).
\end{align*}
The orientation needed for the pointwise comparison is the inverse path
\begin{align*}
f(\ttstar) = r(\ttstar).
\end{align*}
Therefore the reflexivity case is proved, and path induction along $\eta_{\top}(x)$ gives a term
\begin{align*}
h(x) : \operatorname{Id}_C(f(x),r(x)).
\end{align*}
Since $x : \top$ was arbitrary, these terms assemble into
\begin{align*}
h : \prod_{x : \top} \operatorname{Id}_C(f(x),r(x)).
\end{align*}
[/guided]
[/step]
[step:Apply function extensionality to obtain propositional uniqueness]
By [citetheorem:9638], applied to the type $\top$, the constant family with value $C$, and the two functions $f,r : \top \to C$, the pointwise identity
\begin{align*}
h : \prod_{x : \top} \operatorname{Id}_C(f(x),r(x))
\end{align*}
induces an identity in the function type:
\begin{align*}
\operatorname{Id}_{\top \to C}(f,r).
\end{align*}
Since $r = \operatorname{rec}_{\top}(f(\ttstar))$ by definition, this is precisely
\begin{align*}
f =_{\top \to C} \operatorname{rec}_{\top}(f(\ttstar)).
\end{align*}
This proves the propositional uniqueness assertion under function extensionality.
[/step]
[step:Separate the judgmental uniqueness clause from the propositional proof]
Assume now that the definitional equality theory includes judgmental eta for $\top$ and judgmental eta for function types. Judgmental eta for $\top$ says that every term $x : \top$ is definitionally equal to $\ttstar$. Hence, for every $x : \top$,
\begin{align*}
f(x) \equiv f(\ttstar).
\end{align*}
The beta computation rule for the recursor gives
\begin{align*}
\operatorname{rec}_{\top}(f(\ttstar))(\ttstar) \equiv f(\ttstar),
\end{align*}
and judgmental eta for $\top$ also gives
\begin{align*}
\operatorname{rec}_{\top}(f(\ttstar))(x) \equiv \operatorname{rec}_{\top}(f(\ttstar))(\ttstar).
\end{align*}
Thus $f$ and $\operatorname{rec}_{\top}(f(\ttstar))$ are judgmentally equal pointwise. By judgmental eta for function types, this pointwise definitional equality yields the meta-theoretic judgmental equality
\begin{align*}
f \equiv \operatorname{rec}_{\top}(f(\ttstar)) : \top \to C.
\end{align*}
This is not an additional inhabitant of an identity type; it is the conditional judgmental uniqueness statement asserted by the theorem.
[/step]
