Empty Type

Definition

The empty type, $⊥$ , is the type with no inhabitants. It is written as $0$ , $0$ , $⊥$ or $Empty$ depending on context.

Properties

Initial in the category of sets.
Propositional by vacuous truth.
For any type $A$ , the function type $⊥ \to A$ is contractible.
$Π x : ⊥. A x ≃ ⊤$
$Σ x : ⊥. A x ≃ ⊥$

Inference Rules

Formation Rules

⊥ : U

Introduction Rules

$⊥$ has no introduction rules. That would be absurd!

Elimination Rule

\frac{x : ⊥ P : ⊥ \to U f : Π x : ⊥. P x}{elim _{⊥} ( P , f , x ) : P x}

This realizes the principle of absurdity.

Computation Rules

$⊥$ has no computation rules.

Induction Principle

For a type family $P : ⊥ \to U$ , there exists a dependent function $f : Π x : ⊥. P x$ . There are no definitional equalities to satisfy since $⊥$ has no point constructors.

References

hott2013-book

Octocurious

Explorer

Definition

Properties

Inference Rules

Formation Rules

Introduction Rules

Elimination Rule

Computation Rules

Induction Principle

See also

References

Graph View

Table of Contents

Backlinks