11.10. The Empty Type

Planned Content

  • What is Empty?

  • Contrast with Unit and False

  • Definitional equality

Tracked at issue #170

🔗inductive type
Empty : Type

The empty type. It has no constructors. The Empty.rec eliminator expresses the fact that anything follows from the empty type.

Constructors

🔗inductive type
PEmpty.{u} : Sort u

The universe-polymorphic empty type. Prefer Empty or False where possible.

Constructors