Preliminaries🔗

To understand the formation rule for function types, we must first consider the universes and the relations between them. We introduce also proof irrelevance, since it lies behind an exceptional case of the rule.

example (p : Prop) (pf₁ pf₂ : p) : pf₁ = pf₂ := rfl

example : Type := Prop

example : Type 1 := Type

example : Type 2 := Type 1
example : Type 3 := Type 2

example : Type = Type 0 := rfl

example : Prop = Sort 0 := rfl
example : Type u = Sort (u + 1) := rfl

example : Sort (u + 1) := Sort u

Formation🔗

An elementary function type is formed as follows.

example (α β : Type) : Type := α → β

Here the types α and β specify the domain and codomain, respectively. The operator → is right-associative, that is,

example (α β γ : Type) : (α → β → γ) = (α → (β → γ)) := rfl

This is often viewed as encoding functions that take two arguments, the first in α and the second in β, and yield a result in γ. We refer to γ as the final codomain. Moreover, we say that the final codomain of a type δ is δ itself whenever δ is not a function type.[…]This unified terminology across all types is used for instance when discussing type constructors and well-formedness requirements of inductive types.

Recall that the codomain of a function may depend on its argument. Consider the following abstract example.

example (I : Type) (X : I → Type) : Type := (i : I) → X i

We refer to (i : I) → X i as a \Pi-type.[…]\Pi-types are also called dependent function types. Such a type can be thought of as encoding an indexed product of sets, \prod_{i \in I} X_i = \left\{\left. f: I \to \bigcup_{i \in I} X_i\ \right| \ f(i) \in X_i,\ i \in I \right\}.

In fact, all function types are \Pi-types. In the elementary case discussed above, the codomain simply does not depend on the argument.

example
  (α : Sort u) (β : Sort v) : (α → β) = ((a : α) → β)
:= rfl

Since a does not appear in the codomain, we can rewrite the type leaving it as a hole.

example
  (α : Sort u) (β : Sort v) : (α → β) = ((_ : α) → β)
:= rfl

def imax_rule (I : Sort u) (X : I → Sort v) :
  Sort (imax u v) := (i : I) → X i

example : Sort (imax _ 0) = Sort 0 := rfl

example : Sort (imax u (v + 1)) = Sort (max u (v + 1))
:= rfl

example (p : Prop) (q : Prop) : Prop := p → q

example (p : Prop) : Sort 0 := p
example (q : Prop) : Sort 0 := q

example : Sort (imax 0 0) = Prop := rfl

example
  (α : Sort u) (P : α → Prop)
  : (∀ a : α, P a) = ((a : α) → P a)
:= rfl

example (α : Sort u) : Sort (max u 1) := α → Prop

example : Sort 1 := Prop

example (α : Sort u) (P : α → Prop) : Prop := (a : α) → P a

example (α : Sort u) (P : α → Prop) (a : α) : Sort 0 := P a

example : Prop = Sort (imax _ 0) := rfl

example : {α : Sort u} → {a : α} → a = a := rfl

example : (α : Sort u) → (a : α) → a = a := @rfl

example (α : Sort u) (a : α) : a = a := @rfl α a

example : (α : Sort u) → (a : α) → a = a := @rfl

example : (α : Type) → (a : α) → a = a := @rfl

example : (α : Prop) → (a : α) → a = a := @rfl

rfl.{u} {α : Sort u} {a : α} : a = a#check rfl

def pi : Type (w + 1) := Type w → Type w

example
  (π : (Type w → Type w) → Type w)
  (Λ : {ξ : Type w → Type w} → ((i : Type w) → ξ i) → π ξ)
  (app : {ξ : Type w → Type w} → π ξ → (i : Type w) → ξ i)
  (β : ∀
    {ξ : Type w → Type w}
    (f : (i : Type w) → ξ i)
    (x : Type w),
    app (Λ f) x = f x
  )
  : 1 = 0
:= False.elim (Counterexample.girard π Λ app β)

example : Sort (imax _ 0) = Prop := rfl

Introduction🔗

Functions are introduced by \lambda-abstraction. As an illustration, we consider the identity function.

def I₁ {α : Sort u} : α → α := λ x ↦ x

Here are some syntactic variations of the same function.

def I₂ {α : Sort u} := λ x : α ↦ x

def I₃ {α : Sort u} := λ (x : α) ↦ x

def I₄ {α : Sort u} (x : α) := x

variable {α : Sort u} in
def I₅ (x : α) := x

def I₆ {α : Sort u} : α → α := (·)

Observe that the codomain is not specified explicitly in these examples. Lean can infer it based on the domain.

The following function taking two arguments ignores the second one.[…]In the context of combinatory logic, this function is called the combinator K.

def K₁ {α β: Type} : α → (β → α) := λ x ↦ (λ _ ↦ x)

Here are some syntactic variations of the same function.

def K₂ {α β: Type} : α → β → α := λ x _ ↦ x

def K₃ {α β : Type} := λ (x : α) (_ : β) ↦ x

def K₄ {α β: Type} (x : α) (_ : β) := x

def K₅ {α β: Type} (x : α) (y : β) := x

def I₁' {α : Sort u} : {_ : α} → α := λ {x} ↦ x

def I₂' {α : Sort u} := λ {x : α} ↦ x

def I₃' {α : Sort u} {x : α} := x

Elimination🔗

Functions are eliminated by application.

example (α β : Type) (f : α → β) (a : α) : β := f a

More generally,

example (I : Sort u) (X : I → Sort v)
  (f : (i : I) → X i) (i : I) :
  X i := f i

Partial application produces a function taking the remaining arguments.

example (α β γ: Type) (f : α → β → γ) (a : α) : β → γ := f a

In contrast, saturated application produces an expression that is not a function.

example (α β γ: Type) (f : α → β → γ) (a : α) (b : β) :
  γ := f a b

Reduction🔗

Recall that having the same normal form is a sufficient condition for two expressions to be definitionally equal. Computing normal forms involves several kinds of reduction. Importantly, an introduction followed immediately by the associated elimination can be reduced. In the case of functions, this is called \beta-reduction.

example (α : Sort u) (β : Sort v) (f : α → β) (a : α) :
  (λ x ↦ f x) a = f a
:= rfl

variable (α : Sort u) (β : Sort v) (f : α → β) (a : α) in
f a#reduce (λ x ↦ f x) a

Although it is not strictly related to functions, we also consider another form of reduction.

def ℕ2 := ℕ × ℕ

example : ℕ2 = (ℕ × ℕ) := rfl

ℕ2#reduce ℕ2

ℕ × ℕ#reduce (types := true) ℕ2

example : I₁ 0 = 0 := rfl

0#reduce I₁ 0

Equality🔗

In addition to reduction, definitional equality identifies certain expressions that differ only by trivial abstraction. This identification is called \eta-equivalence. For functions, \eta-equivalence says that a function is definitionally equal to the \lambda-abstraction obtained by applying the function to an argument.

example (α : Sort u) (β : Sort v) (f : α → β)
  : (λ x ↦ f x) = f
:= rfl

The definitional equality of the left and right-hand sides is not based on them having the same normal form. In fact, the left-hand side does not reduce.

variable (α : Sort u) (β : Sort v) (f : α → β) in
fun x ↦ f x#reduce λ x ↦ f x

Reduction and \eta-equivalence differ in a fundamental way: the former has an intensional nature while the latter is a limited kind of extensionality.

The principle of functional extensionality holds in Lean, but not by rfl.[…]We give a proof of funext later.

example (α : Sort u) (β : Sort v) (f g : α → β)
  (h : ∀ (x : α), f x = g x)
  : f = g
:= funext h

Local definitions🔗

Consider the following function.

def pq₁ (x : ℕ) : ℕ :=
  (x + 1)^2 + 3*(x + 1) + 1

We can avoid repeating the expression x + 1 by composing two functions.

def q (x : ℕ) : ℕ := x + 1
def p (y : ℕ) : ℕ := y^2 + 3*y + 1
def pq₂ (x : ℕ) := p (q x)

This introduces two names p and q. Such auxiliary definitions can be avoided as follows.

def pq₃ (x : ℕ) :=
  have y := x + 1
  y^2 + 3*y + 1

Here have is syntactic sugar for \lambda-abstraction and application.

example (α : Sort u) (β : Sort v) (a : α) (b : β) :
  (
    have x : α := a
    b
  ) = (λ x : α ↦ b) a := rfl

The parentheses around the have syntax can be omitted.

example (α : Sort u) (β : Sort v) (a : α) (b : β) :
  have x : α := a
  b = (λ x : α ↦ b) a := rfl

In particular, the following coincides with pq₂.

def pq₄ (x : ℕ) :=
  (λ y ↦ y^2 + 3*y + 1) (x + 1)

example (α : Sort u) (P Q : α → Prop)
  (h1 : ∀ a : α, P a → Q a) (h2 : ∀ a : α, P a)
  : ∀ a : α, Q a
:=
  λ a : α ↦
  have Pa := h2 a
  h1 a Pa

example (α : Sort u) (P Q : α → Prop)
  (h1 : ∀ a : α, P a → Q a) (h2 : ∀ a : α, P a)
  : ∀ a : α, Q a
:=
  λ a : α ↦
  have : P a := h2 a
  h1 a this

example (α : Sort u) (P Q : α → Prop)
  (h1 : ∀ a : α, P a → Q a) (h2 : ∀ a : α, P a)
  : ∀ a : α, Q a
:=
  λ a : α ↦
  have : P a := h2 a
  h1 a ‹P a›

def pq₅ (x : ℕ) : ℕ :=
  let y := x + 1
  y^2 + 3*y + 1

def I₇ {α : Sort u} :=
  let t := α
  λ x : t ↦ x

example : (let t := ℕ; t × t) = (ℕ × ℕ) := rfl

ℕ × ℕ#reduce (types := true) (let t := ℕ; t × t)

example : I₇ 0 = 0 := rfl

0#reduce I₇ 0

On inference of implicit arguments🔗

Implicit arguments let us omit information that Lean can usually infer from the surrounding context. As an illustration, we return to the two syntactic variants I₁ and I₂ of the identity function. They both take an implicit argument, denoted by α in the following examples.

example : {α : Sort u} → α → α := I₁

example : {α : Sort u} → α → α := I₂

In the next example, the implicit argument is inferred to be ℕ.

example : I₁ 0 = I₂ 0 := rfl

The inference can stall if the surrounding context is not informative enough. While α appears on the left-hand side of : in the following example, nothing fixes it on the right-hand side, that is, in I₁ = I₂.

example (α : Sort u) : don't know how to synthesize implicit argument `α`
  @Eq (?m.4 α → ?m.4 α) I₁ I₂
context:
α:Sort u⊢ Sort ?u.5

Note: Because this declaration's type has been explicitly provided, all parameter types and holes (e.g., `_`) in its header are resolved before its body is processed; information from the declaration body cannot be used to infer what these values should bedon't know how to synthesize implicit argument `α`
  @I₁ (?m.4 α)
context:
α:Sort u⊢ Sort ?u.5

Note: Because this declaration's type has been explicitly provided, all parameter types and holes (e.g., `_`) in its header are resolved before its body is processed; information from the declaration body cannot be used to infer what these values should beI₁ = don't know how to synthesize implicit argument `α`
  @I₂ (?m.4 α)
context:
α:Sort u⊢ Sort ?u.5

Note: Because this declaration's type has been explicitly provided, all parameter types and holes (e.g., `_`) in its header are resolved before its body is processed; information from the declaration body cannot be used to infer what these values should beI₂ := rfl

To prove the equality of I₁ and I₂, we must provide more information or use the explicit versions.

example (α : Sort u) : (I₁ : α → α) = I₂ := rfl

example : @I₁ = @I₂ := rfl

Perhaps the cleanest way to specify implicit arguments is to use named arguments.

example (α : Sort u) : I₁ (α := α) = I₂ := rfl

example (β : Sort u) : I₁ (α := β) = I₂ := rfl

The left-hand side of := in (α := α) refers to the argument α in the definition of I₁ and the right-hand side to the argument of the anonymous function defined by the example. The second example renames the latter argument to make the distinction visible.

The variant of the identity function taking only implicit arguments is harder to disambiguate: fixing α alone is not enough.

example (α : Sort u) : don't know how to synthesize implicit argument
  @I₁' α (?m.5 α)
context:
α:Sort u⊢ α

Note: Because this declaration's type has been explicitly provided, all parameter types and holes (e.g., `_`) in its header are resolved before its body is processed; information from the declaration body cannot be used to infer what these values should beI₁' (α := α) = don't know how to synthesize implicit argument `x`
  @I₂' α (?m.6 α)
context:
α:Sort u⊢ α

Note: Because this declaration's type has been explicitly provided, all parameter types and holes (e.g., `_`) in its header are resolved before its body is processed; information from the declaration body cannot be used to infer what these values should beI₂' := rfl

Nonetheless, the explicit versions of I₁' and I₂' coincide.

example : @I₁' = @I₂' := rfl

Unlike I₁', whose second argument is anonymous, the second arguments of I₂' and I₃' are both named x and can be referred to as follows.

example (α : Sort u) (x : α)
  : I₂' (x := x)  = I₃' (x := x) := rfl

Here α can be inferred since it is the type of x.

Rules of the type theory🔗

The following rules govern the concepts introduced so far. They constitute a pure type system. For each rule, we first present an example and then its abstract formulation. In the abstract formulations, we write \operatorname{Sort}_{u} for Sort u, \Pi x : \alpha.\; \beta for (x : α) → β x, and \equiv for definitional equality. Moreover, \Gamma denotes an arbitrary typing context and \beta[x := a] denotes substitution.[…]The substitution replaces all free occurrences of x in the expression \beta with the expression a. We use the standard notation for typing rules.

1. Axioms

example : Sort (u + 1) := Sort u

\frac{ }{ \vdash \operatorname{Sort}_{u} : \operatorname{Sort}_{u + 1} }

2. Start

example (α : Sort u) (a : α) : α := a

\frac{ \Gamma \vdash \alpha : \operatorname{Sort}_{u} }{ \Gamma, a : \alpha \vdash a : \alpha }

3. Weakening

example (α : Sort u) (a : α) (β : Sort v) (b : β) : α := a

\frac{ \Gamma \vdash a : \alpha \quad \Gamma \vdash \beta : \operatorname{Sort}_v }{ \Gamma, b : \beta \vdash a : \alpha }

4. Product[…]This is the impredicative maximum rule.

example (α : Sort u) (β : α → Sort v) :
  Sort (imax u v) := (x : α) → β x

\frac{ \Gamma \vdash \alpha : \operatorname{Sort}_{u} \quad \Gamma, x : \alpha \vdash \beta : \operatorname{Sort}_{v} }{ \Gamma \vdash \Pi x : \alpha.\; \beta : \operatorname{Sort}_{\operatorname{imax} u \; v} }

5. Application

example (α : Sort u) (β : α → Sort v)
  (f : (x : α) → β x) (a : α) :
  β a := f a

\frac{ \Gamma \vdash f : \Pi x : \alpha.\; \beta \quad \Gamma \vdash a : \alpha }{ \Gamma \vdash f\; a : \beta[x := a] }

6. Abstraction

example (α : Sort u) (β : α → Sort v)
  (f : (a : α) → β a) :
  (a : α) → β a := λ x ↦ f x

\frac{ \Gamma, x : \alpha \vdash e : \beta \quad \Gamma \vdash \Pi x : \alpha.\; \beta : \operatorname{Sort}_{v} }{ \Gamma \vdash \lambda x : \alpha \mapsto e : \Pi x : \alpha.\; \beta }

7. Conversion

example (α : Sort u) (a : α) :
  let β := α
  β := a

\frac{ \Gamma \vdash a : \alpha \quad \Gamma \vdash \alpha\equiv\beta }{ \Gamma \vdash a : \beta }

Further proofs🔗

example : @I₁ = @I₂ := rfl
example : @I₁ = @I₃ := rfl
example : @I₁ = @I₄ := rfl
example : @I₁ = @I₅ := rfl
example : @I₁ = @I₆ := rfl
example : @I₁ = @I₇ := rfl
example : @I₁ = @I₁' := rfl

example : @K₁ = @K₂ := rfl
example : @K₁ = @K₃ := rfl
example : @K₁ = @K₄ := rfl
example : @K₁ = @K₅ := rfl

example : @I₁' = @I₂' := rfl
example : @I₁' = @I₃' := rfl

example : pq₁ = pq₂ := rfl
example : pq₁ = pq₃ := rfl
example : pq₁ = pq₄ := rfl
example : pq₁ = pq₅ := rfl