Empty type

The empty type, which we denote by $⊥$ ,¹ is motivated in several ways:

$⊥$ is the definitionally false proposition under propositions as types, i.e. a proposition with no proof (in the empty context)
$⊥$ is an empty type, analogous to the empty set $\emptyset$ in set theory.
$⊥$ is an initial type.

A slight wrinkle: We can declare a variable of type $⊥$ as part of a context, therefore it is incorrect to say $⊥$ is empty in all contexts. It is better to have a type-theoretic equivalent of Ex falso quodlibet. This leads naturally to ^E3: In any context, $⊥$ is the smallest type.

Standard presentation

Here we give a formal presentation of $⊥$ in the cartesian calculus of substitutions, following Principles of dependent type theory. #m/def/type/ind The formation rule along is

Γ ⊢ Γ ⊢ ⊥ (⊥) Δ ⊢ 𝛾 : Γ Δ ⊢ ⊥ [𝛾] = ⊥ (⊥ - N) .

$⊥$ is an inductive type with no constructors. Thus there are no introduction rules, and the induction principle gives the elimination rule

Γ ⊢ 𝑏 : ⊥ Γ . ⊥ ⊢ 𝐴 Γ ⊢ 𝐚 𝐛 𝐬 𝐮 𝐫 𝐝 (𝑏) : 𝐴 [𝐢 𝐝 𝑏] (⊥ E) .

Δ ⊢ 𝛾 : Γ Γ ⊢ 𝑏 : ⊥ Γ . ⊥ ⊢ 𝐴 Δ ⊢ 𝐚 𝐛 𝐬 𝐮 𝐫 𝐝 (𝑏) [𝛾] = 𝐚 𝐛 𝐬 𝐮 𝐫 𝐝 (𝑏 [𝛾]) : 𝐴 [𝛾 . 𝑏 [𝛾]] (⊥ E - N) .

We omit an $𝜂$ -unicity rule in the standard presentation, since it can be shown given an Extensional equality type.

Internalizing judgemental structure

In terms of Internalizing judgemental structure, we have for any context $Γ$

⊥ Γ \in T y (Γ),

and for any dependent type $Γ . ⊥ ⊢ 𝐴$ we have

𝜌 Γ, 𝐴 : T m (Γ . ⊥, 𝐴) ≅ {⋆} .

#state/develop | #lang/en | #SemBr

Pronounced “bottom.” ↩

Empty type

Standard presentation

Internalizing judgemental structure

Footnotes