# Lecture 4.1: Mathematics — Foundation

We review the logical foundation of Lean and introduce the axiom of choice, the law of excluded middle, and quotients

## Type universes

Where do types live? We learned that `Prop : Type`, but what about `Type`?

More generally, there is `Sort u`, which forms an infinite sequence of type universes: ```Sort u : Sort (u + 1)```

Important: The universes `u` in `Sort u` are not terms; they consist of variables `u`, zero `0`, successor `_ + 1`, `max`, and `imax`

``````Prop   := Sort 0
Type u := Sort (u + 1)
Type   := Type 0
Type*  := Type _

Sort 0 : Sort 1 : Sort 2 : ...
Prop   : Type 0 : Type 1 : ...
``````

Lean's type hierarchy is noncumulative: Each type lives only in one universe

(This is different in Coq, where `p : Type u` implies `p : Type v` for all `v ≥ u`)

We can use `ulift : Type u → Type (max u v)` to transport types between type universes

Constants can also be polymorphic in the type universe, and can be annotated with type universes—e.g. `eq.{u}`

## Impredicativity

We need the whole `Type` hierarchy to avoid paradoxes

If we had `Type : Type`, we would end up with Girard's paradox, which is analogous to Russel's paradox in set theory

Typing rule for `Π`, including universes:

``````Γ ⊢ α : Sort u   Γ, a : α ⊢ β a : Sort v
————————————————————————————————————————— Pi
Γ ⊢ (Πa : α, β a) : Sort (imax u v)
``````

where

``````imax u 0 = 0
imax u v = max u v   if v ≠ 0
``````

In particular:

``````⊢ α : Sort u    (a : α) ⊢ β a : Prop
————————————————————————————————————— Pi
⊢ (Πa : α, β a) : Prop

⊢ α : Type u    (a : α) ⊢ β a : Type v
——————————————————————————————————————— Pi
⊢ (Πa : α, β a) : Type (max u v)
``````

In particular, in the last instance, `Πα : Type 0, β α` cannot be in `Type 0`

Type constructors such as `list` live in `Type 1` or beyond

The special behavior of the `Pi` rule for `Prop` is called impredicativity

`Prop` is impredicative

`Type` is predicative

Impredicativity works because Lean has proof irrelevance

## Proof irrelevance

What is the difference between `Prop` and `Type`?

Each proposition (when interpreted as a type) is either empty or has exactly one inhabitant: `Prop` = {∅, {⋆}}

``````∀(p : Prop) (h₁ h₂ : p), h₁ = h₂
``````

This is called proof irrelevance and makes reasoning about dependent types easier

Proof irrelevance is implemented in the kernel, which gives us definitional equality, allowing proofs `by refl`

In contrast:

• Agda and Coq are proof relevant by default (but are compatible with proof irrelevance)

• Homotopy type theory and other constructive or intuitionistic type theories build on data in equality proofs and therefore are incompatible with proof irrelevance

`Prop` is an instance of `subsingleton α := ∀a b : α, a = b`

(Other subsingletons: `unit`, `empty`, `decidable P`, ...)

## Large elimination

Compare the following definitions, which are identical except for their type universe (`Prop` vs. `Type`):

``````inductive nonempty (α : Sort u) : Prop
| intro (val : α) : nonempty

inductive inhabited (α : Sort u) : Sort (max 1 u) :=
| mk (default : α) : inhabited
``````

For `inhabited`, we can define `default {α : Type} : inhabited α → α` as the projection of `mk`'s argument:

``````∀a : α, default (inhabited.mk a) = a
``````

We call this large elimination, because we are eliminating into a large type universe (`Type _`)

A similar projection for `nonempty` is explicitly disallowed by Lean, because it would be inconsistent with proof irrelevance

Assume we have a projection function `witness {α : Type} : nonempty α → α` with a computational rule

``````∀a : α, witness (nonempty.intro a) = a
``````

Then

``````example : false :=
have tt ≠ ff :=
have wnw : witness ⟨tt⟩ ≠ witness ⟨ff⟩ :=
by simp only [witness_eq]; assumption,
show false, from
wnw rfl
``````

Thus, there cannot be a computational projection `witness {α : Type} : nonempty α → α`; but there can be a noncomputational one, as we will see in a moment

In general, inductive definitions `c` living in `Type` give rise to a large eliminator:

``````c.elim {α : Sort u} : ∀{p : Sort v}, c α → ... → p
``````

## Small elimination

If we could not eliminate `nonempty`, then it would be completely useless

Fortunately, we can eliminate it, but only into `Prop`; we call this small elimination

Elimination is provided by the following small eliminator:

``````nonempty.elim {α : Sort u} : ∀{p : Prop}, nonempty α → (α → p) → p
``````

For comparison, this is what the large eliminator would look like, if it were allowed:

``````nonempty.elim {α : Sort u} : ∀{p : Sort v}, nonempty α → (α → p) → p
``````

Using it, we could construct a `witness` projection from `nonempty.elim` into `Type`

In general, inductive definitions `c` living in `Prop` give rise to a small eliminator:

``````c.elim {α : Sort u} : ∀{p : Prop}, c α → ... → p
``````

However, if `c` is a "syntactic subsingleton" (e.g. `false`, `∧`, `=`, `well_founded`), a large eliminator is generated

A "syntactic subsingleton" is an inductive definition with at most one constructor whose arguments are either `Prop` or appear as immediate arguments in the output type

This exception is called subsingleton elimination

## Axiom of choice

The axiom of choice is a noncomputational projection from `nonempty`:

``````axiom classical.choice {α : Sort u} : nonempty α → α
``````

It provides an arbitrary element in `α` but gives no information about it

Often we are only interested in having some witness of `∃a : α, p a`, without caring about which one:

``````classical.some : (∃a : α, p a) → α
classical.some_spec (h : ∃a : α, p a) : p (some h)
``````

From `choice`, we can derive several other rules:

• `choice` is equivalent to Zorn's lemma and the well-ordering theorem

• `choice` implies the axiom of choice: `(∀a : α, ∃b : β, r a b) ↔ (∃f, ∀a, r a (f a))`

• `choice` implies the law of excluded middle (LEM or EM): `∀p : Prop, p ∨ ¬ p`

With LEM everything is decidable: `classical.prop_decidable` (Diaconescu’s theorem; see Theorem Proving in Lean, Section 11.6)

`choice` is the only axiom that allows us to construct elements living in `Type` (cf. `funext` and `propext`)

When using `choice` outside of `Prop`, we need to mark the definition as `noncomputable`

## Quotient types

Quotient types are a powerful construction in mathematics

They are used to construct `ℤ`, `ℝ`, and many other types

They are built into Lean; for each relation `r : α → α → Prop`, `quot r` constructs a quotient type with the embedding function `quot.mk r a` (written `⟦a⟧`) and the axiom `quot.sound`:

``````∀a b : α, r a b → ⟦a⟧ = ⟦b⟧
``````

We can lift functions from `α → β` into `quot r → β` using `quot.lift`, which has the following computation rule:

``````quot.lift f h ⟦a⟧ = f a   for h : ∀a b, r a b → f a = f b
``````

We can think of `quot.lift` as an eliminator

If `r` is an equivalence relation, we can derive `⟦a⟧ = ⟦b⟧ ↔ r a b` from `quot.sound`

`quotient` provides a convenient interface for equivalence relations on top of `quot`, including `quotient.lift_on` (for unary functions) and `quotient.lift_on₂` (for binary functions)

## Demo

`41_lecture.lean`