Unit type

The unit type, which we denote by $⊤$ ,¹ is motivated in several ways:

$⊤$ is the definitionally true proposition under propositions as types (see also subobject classifier).
$⊤$ is a singleton.
$⊤$ is a space with only trivial homotopy groups, i.e. no holes of any dimension.
$⊤$ is the terminal type.

The core idea is that in absolutely any context $Γ$ , there is one and only one term $Γ ⊢ 𝐭 𝐭 : ⊤$ , so that all terms of $⊤$ are judgementally equal to $𝐭 𝐭$ .

Standard presentation

Here we give a formal presentation of $𝚷$ -types in the cartesian calculus of substitutions, following Principles of dependent type theory. #m/def/type The formation and introduction are given by

Γ ⊢ Γ ⊢ ⊤ (⊤) Γ ⊢ Γ ⊢ 𝐭 𝐭 : ⊤ (⊤ I)

while we also have the substitution naturality rule

Δ ⊢ 𝛾 : ⊤ Δ ⊢ ⊤ [𝛾] = ⊤ (⊤ - N)

and $𝜂$ -unicity rule

Γ ⊢ 𝑎 : ⊤ Γ ⊢ 𝑎 = 𝐭 𝐭 : ⊤ (⊤ 𝜂)

There is no need for an elimination rule or introduction substitution naturality rule.

Internalizing judgemental structure

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

⊤ Γ \in T y (Γ), 𝜄 Γ : T m (Γ, ⊤) ≅ {⋆} .

#state/tidy | #lang/en | #SemBr

Pronounced “top.” ↩

Unit type

Standard presentation

Internalizing judgemental structure

Footnotes