← Terminology encountered before it is fully explained Index Next: Exercises →

Recall

Formal definitions cited in this section, gathered here for quick reference (full citations in the Bibliography):

Section 3 built Π-types concretely, from Fin n and Vec.replicate, up to the general pattern $\prod_{x:A} B(x)$. This section adds the second half of the picture — Σ-types, the dependent pair dual to the Π-type — and then zooms out to name the whole formal system these pieces belong to: the calculus of constructions (CoC), the core type theory underlying Lean. (Universes get their own formal typing rule in Chapter 5, Section 3, once Chapter 5 has built up the informal picture of Type/Type 1 those rules formalize — nothing here depends on having read that yet.)

Π-types, briefly recalled

\[\prod_{x : A} B(x)\]

— “a function that, given $x : A$, returns a term of type $B(x)$, a type allowed to mention $x$.” Section 3’s Vec.replicate, with type (n : Nat) → Vec α n, literally is $\prod_{n:\mathtt{Nat}} \mathrm{Vec}\,\alpha\,n$; Lean’s surface syntax (x : A) → B x is $\prod_{x:A} B(x)$, and ∀ is the same construct specialized to B : A → Prop, as Chapter 3 makes precise. Every ∀ n : Nat, P n written from that point on is already a Π-type in exactly this sense.

Programmer’s corner (Python), on what is genuinely missing. Even Python’s TypeVar (its own fix for generic functions like identity) cannot express Vec.replicate’s type:

from typing import TypeVar
T = TypeVar("T")

def identity(x: T) -> T:      # generic over a TYPE — fine, this is TypeVar's job
    return x

# There is no Python type-hint equivalent of:
#   def replicate(a: T, n: <this specific Nat>) -> Vec[T, <that same Nat>]
# because "the type mentions n's VALUE" is not expressible by any
# combination of ordinary hints or TypeVar.

This is the honest answer to why Lean needs a whole extra concept here: it is not that Python’s type hints are missing a minor convenience, it is that no mainstream static type system — Python’s, Java’s, C#’s, TypeScript’s — has a construct for “the type mentions a specific runtime value,” because none of them needed a proof assistant’s level of precision. Π-types are precisely that missing construct, made rigorous.

A second worked example, where the codomain is a genuinely different type, not just a differently-sized version of the same type. Vec.replicate always returns some Vec; the following function returns a Nat or a Bool depending on which was asked for — an even sharper case of “the type mentions the argument’s value”:

def pick (b : Bool) : (if b then Nat else Bool) :=
  match b with
  | true => (42 : Nat)
  | false => (true : Bool)

#check @pick   -- pick : (b : Bool) → if b = true then Nat else Bool
#eval pick true   -- 42
#eval pick false  -- true

A counterexample. Forcing pick’s result to a single fixed type (dropping the dependency) is rejected outright, because the two branches genuinely disagree on type — there is no ordinary, non-dependent function type that could describe pick:

def badPick (b : Bool) : Nat :=
  match b with
  | true => 42
  | false => true

error: Type mismatch
  true
has type
  Bool
but is expected to have type
  Nat

Prop as a special, proof-irrelevant universe

Lean’s Prop (Chapter 3) sits alongside Type as its own universe, with one extra rule: proof irrelevance. Any two terms of the same type P : Prop are considered definitionally equal, since a proof carries no computational content beyond the bare fact that a proof exists:

theorem two_proofs (h1 h2 : 2 + 2 = 4) : h1 = h2 := rfl

rfl succeeds no matter how h1 and h2 were each proved — by rfl directly, by a long tactic block, by an entirely different chain of lemmas — because Lean does not distinguish between different proofs of the same Prop. This is what makes Curry–Howard’s slogan “propositions are types, proofs are terms” more than a slogan: P : Prop really is a type, h : P really is an ordinary term of that type built by ordinary $\lambda$/application/Π-type machinery, and the only difference from an ordinary Type is that Lean does not care which term of P was produced — only that one was produced.

Σ-types: the dependent pair, dual to the Π-type

Where the Π-type generalizes the ordinary function type $\to$, a Σ-type (dependent pair / dependent sum) generalizes $\times$ (the ordinary product):

\[\sum_{x:A} B(x)\]

a pair $\langle a, b\rangle$ with $a : A$ and $b : B(a)$ — the second component’s type is allowed to depend on the first component’s value.

Why “sum,” if it generalizes ×? The name is not a mismatch between the Σ-type and the product — it names the more fundamental view underneath both. $\sum_{x:A} B(x)$ is, categorically, a disjoint union (coproduct) of the family $B$ indexed by $A$: one tagged copy of $B(x)$ for every $x \in A$, glued together as separate parts that never overlap. Chapter 3, Section 1’s Curry–Howard table will list ∧ as a product type and ∨ as a sum (coproduct) type, side by side with ∃ as a Σ-type — as though all three were unrelated rows. They are not: ∧ and ∨ are both special cases of this same Σ-type construction. Which connective you get depends on which of the two ingredients — the index type $A$ or the family $B$ — is held fixed and which is allowed to vary:

The Σ-type is called a sum because it always literally is an indexed disjoint union. The product reading (×, and ∧ as its Prop special case) is just the constant-family special case of that same construction, not a second, unrelated thing.

The same split applies to the Π-type, the other way round. $\prod_{x:A} B(x)$ is always literally an indexed product. For a constant family, this collapses to the ordinary function type $A \to B$ (an exponential, written $B^A$) — not to $A \times B$. This is why the Π-type is never confused with × the way the Σ-type is with ∨, and no equivalent puzzle arises on that side.

This shape has already appeared, without the name: Section 3’s Fin n is, under the hood, exactly this pair —

#print Fin
-- structure Fin (n : Nat) : Type
-- fields:
--   Fin.val  : Nat
--   Fin.isLt : val < n

a Nat value val, paired with a proof isLt whose statement (val < n) mentions val itself. That is $\Sigma$, concretely: the second field’s type depends on the value of the first. Here is the general construct, spelled out with Lean’s actual Sigma, pairing a bound with an actual number below it:

def mySigma : Σ n : Nat, Fin n := ⟨3, ⟨2, by decide⟩⟩
#eval mySigma.fst        -- 3
#eval mySigma.snd.val    -- 2

mySigma.fst extracts the first component with no fuss at all — it is ordinary data, just like extracting .1 from an ordinary pair. This extractability matters, because it is exactly what ∃ (next) does not allow, and the reason why is the most subtle point in this section.

A second worked example, mirroring the Π-type one above. Just as a Π-type’s codomain can be a genuinely different type per argument, a Σ-type’s second component can be a genuinely different type per first component — not just a differently-sized version of one fixed type:

def mySigma2 : Σ b : Bool, if b then Nat else String :=
  ⟨true, (42 : Nat)⟩
def mySigma3 : Σ b : Bool, if b then Nat else String :=
  ⟨false, "hi"⟩

#eval mySigma2.fst  -- true
#eval mySigma2.snd  -- 42
#eval mySigma3.fst  -- false
#eval mySigma3.snd  -- "hi"

A counterexample. The second component’s type is dictated by the specific value supplied as the first component, not freely choosable alongside it — supplying a String alongside true (whose dependent type here is Nat) is rejected:

def badSigma : Σ b : Bool, if b then Nat else String :=
  ⟨true, "oops"⟩

error: Application type mismatch: The argument
  "oops"
has type
  String
but is expected to have type
  if true = true then Nat else String
in the application
  ⟨true, "oops"⟩

This dependent-pair shape is also the “structure bundling data + proofs” pattern that recurs throughout this book: Group G’s ⟨op, id, inv, assoc, ...⟩ is, underneath Lean’s structure sugar, an iterated Σ-type — a witness op, paired with a witness id, paired with assoc, whose type depends on the values of op and id supplied earlier in the same structure. This dependent-pair shape is exactly what lets Chapter 2 say that structures can bundle proofs alongside data: every such structure is, underneath, silently an appeal to the Σ-type.

A caveat about ∃, worth being precise about. Chapter 3 will read ∃ x : α, P x as “a structure: a witness value plus a proof that the witness satisfies P” — in effect a Σ-type, with P : α → Prop playing the role of B. Lean’s actual Exists is, however, not literally the Σ-type Sigma. Exists is specifically built to land in Prop, and by proof irrelevance (above), that means the witness cannot be extracted from an ∃-proof computationally:

def bad (h : ∃ n : Nat, n > 0) : Nat := h.1

error(lean.projNonPropFromProp): Invalid projection: Cannot project a
value of non-propositional type
  Nat
from the expression
  h
which has propositional type
  ∃ n, n > 0

Compare this directly to mySigma.fst two paragraphs up, which worked with no error at all — same pair-shape, different universe, and that difference is exactly why one extracts and the other does not. If ∃ did allow extracting a witness, two different (but both equally valid) choices of witness could produce different results from a “proof-irrelevant” input, contradicting proof irrelevance itself. Sigma (the actual, Type-valued dependent pair, matching a structure’s bundled data) does support projecting out its first component, precisely because it does not carry Exists’s irrelevance guarantee. So: ∃ has the same shape as the Σ-type but lives in a universe where the witness is unobservable. That is what makes it a restricted cousin of the Σ-type rather than literally the Σ-type. The structure-based bundling this book uses throughout for Group/Ring/Module genuinely is Sigma-like (extractable), while an ∃-statement genuinely is not.

Π-types and Σ-types, side by side

Everything above in one table, gathering the two constructs’ notation, readings, and special cases for direct comparison:

Aspect Π-type $\prod_{x:A} B(x)$ Σ-type $\sum_{x:A} B(x)$
Read as “for every $x:A$, a term of $B(x)$” “some $x:A$, together with a term of $B(x)$”
Generalizes $A \to B$ (function type) $A \times B$ (product type)
Constant-family collapse ($B$ ignores $x$) ordinary function type $A \to B$ ordinary product $A \times B$
Categorical reading indexed product indexed coproduct (disjoint union)
Lean surface syntax (x : A) → B x Σ x : A, B x, built with ⟨_, _⟩
Logic special case ($B : A \to \mathrm{Prop}$) ∀ x, P x ∃ x, P x
Witness/value extraction always — applying a Π-typed function to an argument is ordinary evaluation allowed for Sigma (Type-valued: .fst/.snd); not allowed for Exists (Prop-valued — proof irrelevance forbids it)
First example this book gave Vec.replicate : (n : Nat) → Vec α n (Section 3 above) Fin n’s own fields, val : Nat paired with isLt : val < n (above)

The one asymmetry worth remembering from the row above: the Π-type’s logic special case (∀) and the Σ-type’s (∃) both extract cleanly as propositions, but only the Σ-type’s data special case (Sigma) supports extracting its witness back out. ∃ looks like a Σ-type and reads like one, but proof irrelevance makes it a strictly weaker, non-extractable cousin — the “caveat about ∃” above is the one place this table’s two columns are not simply mirror images of each other.

Recursors and eliminators, named

Chapter 1, Section 4 promised a formal treatment of the recursor (also called an eliminator) once Π/Σ-types were available; here it is. For an inductive type like Nat, with constructors zero : Nat and succ : Nat → Nat, the recursor Nat.rec is the single term that makes “define a function, or prove a statement, by giving one case per constructor” precise:

#check @Nat.rec
-- {motive : Nat → Sort u}
--   → motive Nat.zero
--   → ((n : Nat) → motive n → motive n.succ)
--   → (t : Nat) → motive t

Read Nat.rec’s own type as a Π-type over a motive motive : Nat → Sort u (Section 4’s “motive,” spelled out in full): supply a “zero case” (a term of motive Nat.zero), a “succ case” (a function turning a value/proof for n into one for n.succ), and Nat.rec produces a term of motive t for any t : Nat. This is structural induction/recursion stated as one Π-typed term rather than as a separate principle bolted onto the language: proving something for zero and showing it is preserved by succ is literally supplying Nat.rec’s two remaining arguments.

A first worked example. The simplest motive is a constant one — the result type does not actually depend on which Nat was supplied, only its value does. Doubling a number, written directly as an application of Nat.rec instead of via +:

def double (n : Nat) : Nat :=
  Nat.rec 0 (fun _ ih => ih + 2) n

#eval double 5   -- 10

Here motive := fun _ => Nat (inferred, since the zero case 0 and the succ case’s result both have type Nat): the zero case supplies 0 for double 0, and the succ case says “given the doubled value ih for n, the doubled value for n.succ is ih + 2” — exactly the recursive definition of doubling, with no separate “recursion” mechanism beyond Nat.rec itself. A dbg_trace inside the succ case makes each of the five hidden recursive steps visible:

def double' (n : Nat) : Nat :=
  Nat.rec 0 (fun _ ih => dbg_trace s!"double: succ case, ih={ih}, adding 2"; ih + 2) n

#eval double' 5
-- double: succ case, ih=0, adding 2
-- double: succ case, ih=2, adding 2
-- double: succ case, ih=4, adding 2
-- double: succ case, ih=6, adding 2
-- double: succ case, ih=8, adding 2
-- 10

Five lines print, one per succ layer Nat.rec peels off 5 = succ(succ(succ(succ(succ zero)))), each showing the running total before the final + 2: 0, then 2, then 4, then 6, then 8, then the returned 10. Nothing about Nat.rec was changed to make this possible — the trace prints from inside the ordinary succ-case function supplied as Nat.rec’s second argument, the same function already described above.

A second worked example, over a different inductive type. The same pattern generalizes to any inductive type, not just Nat. Computing a list’s length via List.rec directly, rather than via the built-in List.length:

noncomputable def myLength {α : Type} (l : List α) : Nat :=
  List.rec (motive := fun _ => Nat) 0 (fun _ _ tailLen => tailLen + 1) l

#reduce myLength [1, 2, 3]        -- 3
#reduce myLength ([] : List Nat)  -- 0

(noncomputable and #reduce in place of #eval here are a Lean implementation detail — the code generator that backs #eval does not yet support compiling List.rec directly, so this definition is checked and reduced by the kernel via #reduce instead; the mathematical content is identical to double above, just for List in place of Nat.) The motive is again constant (fun _ => Nat), the “nil case” is 0, and the “cons case” says “given the tail’s length tailLen, the length with one more element prepended is tailLen + 1.”

Unlike double above, myLength’s recursion cannot be watched with dbg_trace: a dbg_trace call placed inside the cons case prints nothing at all under #reduce, verified directly — the kernel’s definitional reduction (what #reduce invokes) is a pure, side-effect-free rewriting process, not a compiled/interpreted evaluation the way #eval is, so dbg_trace’s print action never fires. This is the same noncomputable boundary from one paragraph up, seen from a second angle: whatever cannot be compiled also cannot be traced by any mechanism that relies on running compiled code.

A counterexample: getting the case order wrong. Nat.rec’s two case arguments are positional, not named — supplying them in the wrong order is a genuine, easy mistake, and Lean rejects it as a type error rather than silently doing the wrong thing:

def doubleBad (n : Nat) : Nat :=
  Nat.rec (fun _ ih => ih + 2) 0 n

error: Type mismatch
  fun x ih => ih + 2
has type
  (x : ?m.4) → (ih : ?m.13 x) → ?m.15 x ih
but is expected to have type
  Nat

The succ-case function was placed where the zero case belongs; since Nat.rec’s first explicit argument must have type motive Nat.zero (here, plainly Nat), a function is rejected on the spot. This is the same class of error underlying “motive is not type correct” messages elsewhere in this book: Nat.rec’s argument positions encode real structure (which case is which), and getting that structure wrong is caught before anything runs, not discovered later at #eval time.

An eliminator is the general name for this same pattern applied to any inductive type: the single term that “uses” a value of that type by case-splitting on which constructor built it, with a motive tracking what is being proved or built in each case. Nat.rec above is Nat’s eliminator; Chapter 3, Section 5’s Or.elim {P Q R : Prop} (h : P ∨ Q) (hpr : P → R) (hqr : Q → R) : R is Or’s — a case for Or.inl and a case for Or.inr, with the (non-dependent, here) motive fixed to the constant type R. Every match/cases/induction used from here on compiles down to exactly this: an application of the relevant inductive type’s eliminator, built automatically rather than written out by hand.

The calculus of constructions, named

Putting the pieces together, the calculus of constructions (CoC, Coquand–Huet) — the core type theory underlying Lean, Coq, and similar systems — is a small formal system built from a variable, a function abstraction, and function application, plus:

  1. an infinite hierarchy of type universes $\mathtt{Type}\,0, \mathtt{Type}\,1, \ldots$, formalized in Chapter 5, Section 3,
  2. Π-types generalizing $\to$, allowing types to depend on terms (this chapter’s Section 3 and the top of this page),
  3. (in Lean’s specific extension, the Calculus of Inductive Constructions, CIC) inductive type declarations — Nat, Bool, Vec/Fin (Section 3), Path (Chapter 11), and every structure written throughout — giving Σ-types and much more (arbitrary recursive data) beyond what bare CoC provides,
  4. Prop as a distinguished, proof-irrelevant universe (Chapter 3, and above), making Curry–Howard a precise correspondence rather than an analogy.

Every single Lean construct used in this book — def, structure, theorem, ∀, ∃, tactics (which merely build CIC terms, one piece at a time, without the terms being written by hand) — compiles down to a term in exactly this system, checked by Lean’s kernel using nothing more than typing rules like the ones sketched here and in Chapter 5, applied mechanically. Chapter 5, Section 3 completes the picture with the simply typed λ-calculus’s typing judgments and its progress/preservation theorems — the formal reason “well-typed proofs do not go wrong” — plus the universe-formation rule only sketched by name above.

References

Full citations in the Bibliography. Formal definitions and verbatim quotes are gathered in Recall, above.

← Terminology encountered before it is fully explained Index Next: Exercises →
Try Lean
Lean playground · v1.4.18 ↗