[proofplan] Fix an arbitrary type $C$. The eliminator for $\bot$ is defined by pattern matching on an assumed input $x : \bot$. Since $\bot$ has no constructors, the pattern match has no branches to specify. The associated computation rule is vacuous, because there is no constructor of $\bot$ on which the recursor could be evaluated. [/proofplan] [step:Define the recursor by empty pattern matching] Let $C$ be a type. Define the function \begin{align*} \operatorname{rec}_{\bot,C} : \bot \to C \end{align*} as the eliminator obtained by case analysis on an input $x : \bot$. This case analysis requires one branch for each constructor of $\bot$. By the defining formation of the empty type, $\bot$ has no constructors. Therefore there are no branches to provide, and the empty case split forms a term $\operatorname{rec}_{\bot,C}(x) : C$ under the assumption $x : \bot$. Abstracting over $x$ gives $\operatorname{rec}_{\bot,C} : \bot \to C$. [guided] We fix a type $C$ and want to construct a map from $\bot$ into $C$. In [type theory](/page/Type%20Theory), a function out of an inductive type is defined by giving one defining clause for each constructor of the source type. Thus, to define a function \begin{align*} \operatorname{rec}_{\bot,C} : \bot \to C, \end{align*} we assume an input $x : \bot$ and perform case analysis on $x$. The key point is that $\bot$ is the empty type: it has no constructors. Hence the usual list of constructor branches is empty. There is no case for a variable of type $\bot$ to fall into, so no term of $C$ has to be supplied as branch data. The empty pattern match is therefore a well-formed term of type $C$ under the assumption that $x$ is a term of type $\bot$: \begin{align*} \operatorname{rec}_{\bot,C}(x) : C. \end{align*} By abstraction over the assumed input $x$, this contextual term determines a function \begin{align*} \operatorname{rec}_{\bot,C} : \bot \to C. \end{align*} This is exactly the ordinary eliminator for the empty type. [/guided] [/step] [step:Verify that the computation rule is vacuous] The computation rule for an inductive eliminator is checked on constructor forms of the source type. Since $\bot$ has no constructors, there is no constructor term of type $\bot$ and hence no computation equation to verify. Thus the empty eliminator satisfies all required computation rules, completing the construction of $\operatorname{rec}_{\bot,C} : \bot \to C$. [/step]