Empty and Unit types

In this chapter, we explore two of the simplest—but most fundamental—types in Lean: the Empty type and the Unit type. Though these types may seem trivial at first glance, they play a crucial role in the logic and structure of formal proofs.

Empty

The Empty type, written as Empty, is a type with no inhabitants.

If we #print Empty, Lean returns:

inductive Empty : Type
number of parameters: 0
constructors:

This means that if we have a value of type Empty, we can derive a value of any other type from it. In Lean, this is done using the Empty.elim function, which expresses the logical principle that from falsehood, anything follows.

emptyToAny

def emptyToAny {A : Type} : Empty → A := by
  intro x
  exact Empty.elim x

An interesting property of the emptyToAny function is that it is unique up to definitional equality; any two functions with type Empty → A are definitionally the same.

emptyToAny

theorem emptyToAnyUnique {A : Type} {f g : Empty → A} : f = g := by
  funext x
  exact Empty.elim x

This implies that the emptyToAny function with codomain Empty is, in particular, the identity function on Empty.

emptyToAny

theorem emptyToAnyId : @emptyToAny Empty = id := by
  funext x
  exact Empty.elim x

Unit

The Unit type, written as Unit, is a type with exactly one inhabitant: Unit.unit, usually just written ().

If we #print Unit, Lean returns:

@[reducible] def Unit : Type :=
PUnit

There is always a function from any type to the Unit type, since we can simply ignore the input and return ().

anyToUnit

def anyToUnit {A : Type} : A → Unit := by
  intro _
  exact ()

The anyToUnit function is unique up to definitional equality; any two functions with type A → Unit are definitionally the same.

anyToUnit

theorem anyToUnitUnique {A : Type} {f g : A → Unit} : f = g := by
  funext x
  exact rfl

This implies that when the domain is Unit, the anyToUnit function is, in particular, the identity function on Unit.

anyToUnit

theorem anyToUnitId : @anyToUnit Unit = id := by
  funext x
  exact rfl

Exercises

Empty

Exercises.lean

-- All the elements of `Empty` are equal
theorem emptyUnique : ∀ (x y : Empty), x = y := by sorry

-- The `emptyToAny` function is injective
theorem emptyToAnyInj {A : Type} : injective (@emptyToAny A) := by sorry

-- Under `Classical.choice`, if the `emptyToAny` function is surjective, the codomain cannot be `Nonempty`
theorem emptyToAnySurj {A : Type} : surjective (@emptyToAny A) ↔ ¬ (Nonempty A) := by sorry

Unit

Exercises.lean

-- All the elements of `Unit` are equal
theorem unitUnique : ∀ (x y : Unit), x = y := by sorry

-- The `anyToUnit` function is injective if, and only if, the domain has only one element
theorem anyToUnitInj {A : Type} : injective (@anyToUnit A) ↔ (∀ (a1 a2 : A), a1 = a2) := by sorry
  
-- Under `Classical.choice`, the `anyToUnit` function is surjective if and only if the domain is `Nonempty`
theorem anyToUnitSurj {A : Type} : surjective (@anyToUnit A) ↔ Nonempty A := by sorry