# 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](https://www.quora.com/What-is-Girards-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 :=
by contradiction,
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`](41_lecture.lean)
## References
* [_Theorem Proving in Lean_](https://leanprover.github.io/theorem_proving_in_lean/) by Jeremy Avigad, et al., Section 3.5, Chapter 11
Further reading:
* [_Homotopy Type Theory: Univalent Foundations of Mathematics_](https://homotopytypetheory.org/book) by the Univalent Foundations Program Institute for Advanced Study