# 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
