## Terminology encountered before it is fully explained

[← Dependent types, with examples](03-dependent-types.md) | [Index](00-index.md) | [Next: Π/Σ-types and the calculus of constructions →](05-pi-sigma-and-coc.md)

---

### Recall

Formal definitions cited in this section, gathered here for quick
reference (full citations in the [Bibliography](../bibliography.md)):

- **Bound / free variable.** "An occurrence of x is free if it
  appears in a position where it is not bound by an enclosing
  abstraction on x" ([Pierce2002], §5.1, p. 55). Brief: inside
  `λx.t`, occurrences of `x` in `t` are bound; any other variable is
  free.
- **α-conversion.** "Church used the term alpha-conversion for the
  operation of consistently renaming a bound variable in a term"
  ([Pierce2002], §5.3, p. 73). Brief: renaming a bound variable does
  not change a term's identity.
- **β-reduction.** "The operation of rewriting a redex according to
  the above rule is called beta-reduction" ([Pierce2002], §5.1,
  p. 56). Brief: applying an abstraction to an argument by
  substitution, $(\lambda x.\, t)\, s \to t[x := s]$.
- **Currying.** "The transformation of multi-argument functions into
  higher-order functions is called currying in honor of Haskell
  Curry" ([Pierce2002], §5.2, pp. 58–59). Brief: a multi-argument
  function is really a chain of one-argument functions returning
  functions.
- **Weak head normal form.** "Weak Head Normal Form: all expressions
  which are either λ-abstractions or of the form
  $\lambda x_1 \ldots \lambda x_n.\, y\, e_1 \ldots e_m$"
  ([Thompson1991], §2.3, p. 36, Definition 2.8). Brief: reduced far
  enough to see the outermost constructor or function head, not
  necessarily any further.
- **Church–Rosser theorem.** "For all $e, f$ and $g$, if $e \to f$
  and $e \to g$ then there exists $h$ such that $f \to h$ and
  $g \to h$" ([Thompson1991], §2.3, p. 38, Theorem 2.10). Brief:
  different terminating reduction orders always reach the same
  normal form.
- **Universal property (general form).** "If $S : D \to C$ is a
  functor and $c$ an object of $C$, a universal arrow from $c$ to $S$
  is a pair $(r, u)$ consisting of an object $r$ of $D$ and an arrow
  $u : c \to Sr$ of $C$, such that to every pair $(d, f)$ with $d$ an
  object of $D$ and $f : c \to Sd$ an arrow of $C$, there is a unique
  arrow $f' : r \to d$ of $D$ with $Sf' \circ u = f$" ([MacLane1998],
  Ch. III §1, p. 55). Brief: a construction characterized by which
  maps *uniquely factor through it*, not by what it is made of.
- **Initial object.** "An object $s$ is initial in a category $C$ if
  to each object $a$ of $C$ there is exactly one arrow $s \to a$"
  ([MacLane1998], Ch. I §5, p. 20). Brief: exactly one morphism out
  to every other object of the category.
- **Forgetful functor.** "A functor which simply 'forgets' some or
  all of the structure of an algebraic object is commonly called a
  forgetful functor (or, an underlying functor)" ([MacLane1998],
  Ch. I §3, p. 14). Brief: a functor that keeps only part of a
  structure, discarding the rest.
- **Subobject.** "Let $A$ be any category. If $u : s \to a$ and
  $v : t \to a$ are two monics [in $A$] with a common codomain $a$,
  write $u \sim v$ when $u$ factors through $v$ ... the corresponding
  equivalence classes of these monics are called the subobjects of
  $a$" ([MacLane1998], Ch. III §7, p. 126; equivalently
  [Pareigis1970], §1.6, p. 20). Brief: a piece of an object cut out
  by a condition, remembered together with its inclusion.
- **Full subcategory.** "We say that $S$ is a full subcategory of
  $C$ when the inclusion functor $S \to C$ is full" ([MacLane1998],
  Ch. I §3, p. 15). Brief: a subcategory retaining *all* original
  morphisms of $C$ between its objects, not just some of them.

---

Four words are going to come up constantly from here on, well before this
book gives any of them a full formal treatment. Rather than leave these
words undefined until they are needed, here is a working definition of
each, good enough to use right away, with pointers to where a fuller
formal treatment lives — [Chapter 1, Section 5](05-pi-sigma-and-coc.md) for
Π/Σ-types and the calculus of constructions, [Chapter 3,
Section 2](../03-propositions-and-proofs/02-logic-recap.md) for the logic
underneath Curry–Howard, and [Chapter 5,
Section 3](../05-rigor-check/03-typing-rules-and-safety.md) for typing rules and
why Lean's guarantees can be trusted.

### Elaborate / elaboration

This is the process by which Lean turns the surface syntax written by the
user into a fully-explicit, fully-typed internal term: filling in implicit
arguments, resolving notation, checking every subterm's type against
what is expected. When this book says an expression "elaborates to"
something, it means "after Lean has finished this filling-in process, the
result is..." For example, `identity 5` *elaborates to*
`@identity Nat 5` (Chapter 1), with `α := Nat` filled in silently.
Elaboration is not guessing: it is **type inference for the calculus of
constructions** ([Chapter 1, Section 5](05-pi-sigma-and-coc.md) makes this system precise),
a deterministic algorithm driven by that calculus's own typing rules, not
black-box compiler behavior. Every "Lean figures it out from context"
moment since the very first `identity 5` is this same algorithm at work.

### Unify / unification

This is the specific step inside elaboration that solves
"what must this placeholder be, given what I already know?" When Lean
sees `identity 5` and knows `identity : {α : Type} → α → α`, it *unifies*
the type of `5` (namely `Nat`) with the placeholder `α`, concluding
`α := Nat`. Unification is what makes implicit-argument inference
(Chapter 1), `apply`'s subgoal-matching (Chapter 4), and typeclass
instance search (Chapter 5) all work. In each case, Lean is solving an
equation between two (possibly partially unknown) terms — a
well-understood, terminating (for the fragment Lean actually uses)
procedure, not an oracle. When it fails, the resulting error message
(Chapter 4, "reading a tactic failure") states specifically which
unification equation could not be solved.

> **Tactics do not add anything to the underlying calculus.** Every tactic
> from Chapter 4 onward ([`intro`](https://lean-lang.org/doc/reference/latest/Tactic-Proofs/Tactic-Reference/), [`exact`](https://lean-lang.org/doc/reference/latest/Tactic-Proofs/Tactic-Reference/), [`rw`](https://lean-lang.org/doc/reference/latest/Tactic-Proofs/Tactic-Reference/), [`induction`](https://lean-lang.org/doc/reference/latest/Tactic-Proofs/Tactic-Reference/), ...) is a
> *user interface* for building terms of this same calculus step by step,
> with the goal state showing the type of the "hole" still to be filled.
> Every finished tactic proof elaborates to an ordinary term that could
> have been written by hand; running `#print` on any tactic-proved theorem
> shows the literal term the tactic script built.

### Reduce / reduction, normal form

A term **reduces** by repeatedly applying its computation rules:
substituting an abstraction's argument into its body (β-reduction),
unfolding a `def`, or simplifying a `match` on a known constructor. A term
with no more reductions available is in **normal form**. `#eval`
(Chapter 1) computes a term's normal form and prints it. `rfl` (Chapter 3)
succeeds exactly when both sides of an equation share a normal form. In
practice, Lean's kernel usually only reduces as far as it needs to
progress: down to **weak head normal form** — far enough to see the
outermost constructor or function head, not necessarily all the way
down. This is why, for example, `Nat.add`'s recursion on its *second*
argument (Chapter 4) determines which side of an equation reduces "for
free" and which needs an explicit inductive argument. Lean only unfolds
`a + b` far enough to expose `b`'s shape, so `a + 0` reduces immediately
(the second argument is already the base case), while `0 + a`, with an
unknown `a` in the position `Nat.add` recurses on, does not reduce at all
until `a` itself is known.

**Where β-reduction comes from, precisely.** Every `fun x => ...` in this
book compiles down to one small formal system, the **λ-calculus**: a
variable `x`, an abstraction `fun x => t` (written $\lambda x.\, t$), or
an application `t1 t2`, and nothing else — no built-in numbers, booleans,
`if`, or recursion; every one of those is *encoded* as a term built from
these three constructs alone. In $\lambda x.\, t$, occurrences of `x`
inside `t` are **bound**; any other variable is **free** — exactly Lean's
ordinary lexical scoping. Two abstractions differing only in a bound
variable's name (`fun a => a` vs. `fun x => x`) are considered the *same*
term (**α-conversion**); Lean's elaborator treats them as interchangeable
without comment. The one computation rule, **β-reduction**, is applying an
abstraction to an argument by substitution:
$$
(\lambda x.\, t)\, s \;\longrightarrow_\beta\; t[x := s]
$$
— precisely definitional equality's engine: `(fun x => x * 2) 5` reduces,
by exactly this rule, to `5 * 2`. Every abstraction takes exactly *one*
argument; a "two-argument function" `fun x y => t` is really `fun x => fun
y => t`, a function returning a function — this is **currying**, why
`Nat → Nat → Nat` is genuinely `Nat → (Nat → Nat)`, one argument at a
time, with no separate multi-argument mechanism underneath. Finally, the
**Church–Rosser theorem** guarantees that if a term has several possible
next reduction steps, reducing them in any order that terminates reaches
the *same* normal form — the theoretical bedrock under never having to
worry that elaborating an expression "the wrong order" gives a different
answer than "the right order."

**Worked example.** Reduce $(\lambda x.\, \lambda y.\, x)\, a\, b$
(application associates to the left, so this is
$((\lambda x.\, \lambda y.\, x)\, a)\, b$):
$$
(\lambda x.\, \lambda y.\, x)\, a\, b
\;\longrightarrow_\beta\; (\lambda y.\, a)\, b
\;\longrightarrow_\beta\; a
$$
The first step substitutes $a$ for $x$ in $\lambda y.\, x$, giving
$\lambda y.\, a$ — note $a$ is now *free* inside this abstraction, since
the original body never mentioned $y$ at all. The second step substitutes
$b$ for $y$ in a body that does not mention $y$, so it simply discards
$b$ and leaves $a$. This particular term — $\lambda x.\, \lambda y.\, x$,
"take two arguments, return the first, discard the second" — is important
enough to have its own name, $K$, and it becomes `Bool.true`'s
implementation once booleans are encoded this way (as in Chapter 13's
Church-encoding aside).

**A second worked example, applying the identity to itself.** Reduce
$(\lambda x.\, x\, x)\, (\lambda y.\, y)$ — this needs *two* β-steps in a
row, each firing on the *outermost* application, unlike the previous
example where the second step fired inside what the first step had just
produced:
$$
(\lambda x.\, x\, x)\, (\lambda y.\, y)
\;\longrightarrow_\beta\; (\lambda y.\, y)\, (\lambda y.\, y)
\;\longrightarrow_\beta\; \lambda y.\, y
$$
The first step substitutes $\lambda y.\, y$ for $x$ in $x\, x$, producing
$(\lambda y.\, y)\, (\lambda y.\, y)$ — the identity function applied to
itself. That is itself a new redex, so a second β-step fires: substituting
$\lambda y.\, y$ for $y$ in the body $y$, leaving $\lambda y.\, y$
unchanged, since applying the identity function to any term just returns
that term. The result, $\lambda y.\, y$, is the identity function again —
applying identity to itself gives back identity.

**A worked example needing α-conversion, not just β-reduction.** Reduce
$(\lambda x.\, \lambda y.\, x)\, y$ — note the *argument* being substituted
in is itself named $y$, the same name as the inner bound variable. Naive,
purely textual substitution would replace $x$ with $y$ inside
$\lambda y.\, x$ and get $\lambda y.\, y$ — but that is *wrong*: it turns
the free $y$ being substituted in into a variable *bound* by the inner
$\lambda y$, silently changing which $y$ is meant (**variable capture**).
Correct, capture-avoiding substitution first α-converts the bound variable
to a fresh name, say $z$, since $\lambda y.\, x$ and $\lambda z.\, x$ are
the same term (α-conversion, as above):
$$
(\lambda x.\, \lambda y.\, x)\, y
\;=\; (\lambda x.\, \lambda z.\, x)\, y
\;\longrightarrow_\beta\; \lambda z.\, y
$$
$\lambda z.\, y$ is the correct result: a function that ignores its
argument and returns the *original free* $y$ — exactly what
$\lambda x.\, \lambda y.\, x$ ("return the first argument, discard the
second") should do when handed $y$ itself as that first argument.
Lean's elaborator performs this renaming automatically and silently, the
same way it treats α-equivalent terms as identical; a book working example
is the only place this step needs to be shown explicitly.

**Programmer's corner (Python).** Python's own `lambda` really does
β-reduce exactly like the calculus above on simple examples —
`(lambda x: x + 1)(5)` reduces to `5 + 1` to `6`, the same substitution
step as $(\lambda x.\, x + 1)\, 5 \to_\beta 5 + 1$ — but Python's
`lambda` is a deliberately limited subset: its body must be a single
*expression*, no `if`/`for`/multiple statements. The actual untyped
λ-calculus has no such restriction, because none is needed: conditionals
and recursion are just more terms built from abstraction and
application, not separate features bolted on top. Lean's `fun` matches
the unrestricted calculus, not Python's narrower `lambda`.

Chapter 1, Section 5 extends exactly this calculus with dependent types (Π/Σ,
universes) to reach the system Lean's kernel actually runs — the
**calculus of constructions**.

### Motive

This is the (possibly type-dependent) predicate or type family that a
tactic like `induction` or `rw` is secretly generalizing the goal over
before it operates. When `rw [h]` fails with **"motive is not type
correct,"** the meaning is as follows: to replace one side of `h` with the
other throughout the goal, Lean first abstracts the goal into a function
`C` (the motive) taking the rewritten term as a parameter. Here, that
abstraction produces an ill-typed `C`, typically because the term being
rewritten appears inside a dependent type's *index* (as in Chapter 11's
`Path`, whose very type depends on specific vertices) rather than in a
position that can vary freely. The fix is almost always to restate the
goal first with `show`, or to generalize the index explicitly, so the
motive Lean builds is well-typed.

**A worked example**, using `Vec` from Section 3 and the dependent pair
`⟨_, _⟩` notation named formally as a Σ-type in [Chapter 1, Section 5](05-pi-sigma-and-coc.md)
(the next section — nothing here depends on that name yet, only on
reading `⟨n, v⟩` as "a `Nat` paired with a `Vec` of that length"):

```lean
example (α : Type) (n : Nat) (h : n = 0) (v : Vec α n) :
    (⟨n, v⟩ : Σ k, Vec α k) = ⟨0, h ▸ v⟩ := by
  rw [h]
```

```
error: Tactic `rewrite` failed: motive is not type correct:
  fun _a => ⟨_a, v⟩ = ⟨0, h ▸ v⟩
```

`n` appears twice in the goal: once as the pair's first component, and
once hidden inside `v`'s own type, `Vec α n`. Abstracting the first
occurrence to build the motive leaves `v` — still fixed at `Vec α n` —
sitting in a slot that now expects `Vec α _a` for an arbitrary `_a`,
which is exactly the ill-typed `C` described above. The fix here is
`subst h` in place of `rw [h]`: `subst` replaces `n` with `0`
*everywhere at once*, including inside `v`'s type, so no intermediate
ill-typed motive is ever built:

```lean
example (α : Type) (n : Nat) (h : n = 0) (v : Vec α n) :
    (⟨n, v⟩ : Σ k, Vec α k) = ⟨0, h ▸ v⟩ := by
  subst h
  rfl
```

> Read more: [Chapter 5, Section 4](../05-rigor-check/04-defeq-vs-propeq.md)
> revisits "motive is not type correct" alongside definitional equality;
> [Chapter 1, Section 5](05-pi-sigma-and-coc.md) shows the recursor/eliminator
> (e.g. `Nat.rec`) whose own type is literally parameterized by a motive,
> which is where the name comes from.

### Category-theory terms used beyond the baseline

This book assumes only "objects, morphisms, composition, functors" as
prior category theory, and the main text holds to that limit throughout.
The optional "Mathematical reading" boxes scattered through later
chapters occasionally go one step further, for readers who already possess
a bit more category theory and would appreciate the extra precision. Four
such terms come up often enough to be worth fixing once here, so every
later use can simply point back to this entry instead of re-explaining
(or, worse, silently assuming) each time:

#### Universal property

This is a characterization of a construction not by what it is *made of*,
but by what maps *uniquely factor through it*. "$X$ has property $U$"
means "for every $Y$ with the relevant data, there is exactly one map
$Y \to X$ compatible with that data." This is the category-theorist's way
of saying "$X$ is the *best possible* solution to a mapping problem," and
it is the same idea as the familiar universal properties of products,
quotients, and free constructions from an algebra course; nothing new is
meant by the phrase here beyond that. Here is the classic picture, for a
product $X \times Y$: given any $A$ with maps to both factors, there is
exactly one map into the product making everything agree (the dashed
arrow):

```mermaid
graph TD
    A -->|f| X
    A -->|g| Y
    A -.->|"∃!h"| P
    P -->|"πX"| X
    P -->|"πY"| Y
```

| Symbol | Lean |
| --- | --- |
| $A$, $X$, $Y$, $P$ ("the objects") | types `A`, `X`, `Y`, `X × Y` |
| $f$, $g$ ("the given maps") | ordinary functions `f : A → X`, `g : A → Y` |
| $\exists!$ ("there exists a unique") | — no single token; witnessed by supplying `h` and proving it is the only one |
| $h$ ("the mediating map") | `fun a => (f a, g a) : A → X × Y` |
| $\pi_X, \pi_Y$ ("the projections") | `Prod.fst`, `Prod.snd` (`.1`/`.2`, or `.fst`/`.snd`) |

Read the diagram as follows: the two solid outer arrows ($f$
and $g$) are *given*. The universal property *asserts* the dashed middle arrow $h$
exists, is unique, and makes both triangles commute: $\pi_X \circ h = f$
and $\pi_Y \circ h = g$, i.e. `h a |>.1 = f a` and `h a |>.2 = g a` for
every `a`. "Commute" just means any two paths between the same two
objects in the diagram compose to the same map. This is exactly what
`⟨_, _⟩` does for `Pair`/`structure` types (Chapter 2, Section 1): give it an
`f`-shaped piece and a `g`-shaped piece, and it hands back the unique `h`
combining them.

**A second example, of a genuinely different shape: a free construction.**
[Chapter 1, Section 1](01-everything-has-a-type.md) already used this idea without
naming it: $(\mathbb{N}, +, 0)$ is the *free commutative monoid on one
generator*. Spelled out, that claim is itself a universal property, with
the "relevant data" this time being "a monoid $M$ together with a chosen
element $m \in M$" (instead of "a pair of maps," as for the product
above):

```mermaid
graph LR
    N["ℕ (with +, 0)"] -.->|"∃!h"| M["M (any monoid)"]
```

"for every monoid $M$ and every element $m \in M$, there is exactly one
monoid homomorphism $h : \mathbb{N} \to M$ with $h(1) = m$" — namely
$h(n) = \underbrace{m + \cdots + m}_{n}$ (iterate $m$'s own operation $n$
times), forced because a homomorphism must send $0$ to $M$'s identity and
send $a+b$ to $h(a)$ combined with $h(b)$. Where the product's mediating
map $h$ was built by pairing ($\langle f, g\rangle$), this $h$ is built by
*iteration*; the common thread is still "exactly one map making the
obvious diagram commute," just with a different shape of "obvious
diagram" and a different notion of "compatible with the given data."
$1 \in \mathbb{N}$ plays the role of the generator being mapped to $m$,
matching $X\times Y$'s two projections $\pi_X,\pi_Y$ above.

#### Initial object

This is an object $I$ of a category with a *unique* morphism
$I \to X$ out to every other object $X$: the universal property above,
specialized to "the best possible source":

```mermaid
graph LR
    I --> X
    I --> Y
    I --> Z
```

| Symbol | Lean |
| --- | --- |
| $I$ ("the initial object") | `Nat` (in `Type`) or `ℤ` (in `Ring`) |
| $I \to X$ ("the unique arrow") | for `Nat`: `Nat.rec` — build a value of *any* `X` by giving a `zero` case and a `succ` case, and that recipe is forced by `Nat`'s two constructors, with no other choice possible |

Exactly one arrow leaves $I$ for every object in the category — never
zero (there is always a map), never more than one (no choice about which).
`Nat` ([Chapter 1, Section 1](01-everything-has-a-type.md)) and
`ℤ` in `Ring` (Chapter 8) are both flagged as initial objects of the
relevant category in this sense: any structure-preserving map out of them
is forced, with no choice involved.

#### Forgetful functor

This is a functor that takes a structure and *keeps only
part of it*, discarding the rest. Examples: the map sending a group $G$ to
its underlying set (forgetting the multiplication), or a `Ring` to its
underlying `Group` under addition (forgetting multiplication and its
unit):

```mermaid
graph LR
    Ring["Ring (R,+,·)"] -->|forgetful| Group["Group (R,+)"]
    Group -->|forgetful| Set["Set (R)"]
```

| Symbol | Lean |
| --- | --- |
| `Ring` $\to$ `Group` ("forgets $\cdot$") | `r.toGroup` (or `r.toAddGroup`, depending on naming) for `r : Ring R` |
| `Group` $\to$ `Set` ("forgets $+$") | `g.carrier`, or simply treating `G : Type` as its own underlying set |

Each arrow keeps *less* structure than the one before it. A `Ring`
remembers both operations, the `Group` it maps to remembers only
addition, and the `Set` it maps to remembers only the underlying elements.
In this book, every `.toGroup`/`.toAddGroup`-style field generated by
Lean's `extends`
([Chapter 2, Section 3](../02-functions-and-structures/03-extending-structures.md)
onward) *is* a forgetful functor,
computationally: it is the projection that keeps some of a structure's
data and drops the rest.

#### Subobject / full subcategory

A subobject of $X$ is (informally) "a
subset of $X$ cut out by some condition, remembered together with its
inclusion into $X$." For example, `CommGroup` is a subobject of `Group`'s
data, cut out by the extra commutativity axiom:

```mermaid
graph LR
    subgraph Group["Group (all groups)"]
        CommGroup["CommGroup (abelian)"]
    end
```

| Symbol | Lean |
| --- | --- |
| $\subseteq$ ("subobject inclusion") | `structure CommGroup (G) extends Group G where comm : ...` |
| $\iota$ ("the inclusion map") | `.toGroup`, the field `extends` generates automatically |

A full subcategory is the category formed by all objects satisfying such
a condition, together with *all* morphisms between them inherited
unchanged from the ambient category. (Nothing is removed at the morphism
level, only at the object level.) For example, abelian groups form a full
subcategory of all groups.

These four are the ones worth fixing once. If a "Mathematical reading" box
elsewhere uses a still-more-specialized term (adjunction, biproduct, a
presheaf category, and the like), treat it as genuinely optional bonus
content for readers who already know it. Nothing later in the book
depends on it, and the surrounding plain-English explanation always stands
on its own without it.

---

### References

Full citations in the [Bibliography](../bibliography.md). Formal
definitions and verbatim quotes are gathered in Recall, above.

- Pierce ([Pierce2002]), §5.1 "Basics," p. 55 — free variables.
- Pierce ([Pierce2002]), §5.1 "Basics," p. 56 — β-reduction.
- Pierce ([Pierce2002]), §5.2 "Programming in the Lambda-Calculus," pp. 58–59 — currying.
- Pierce ([Pierce2002]), §5.3 "Formalities," p. 73 — α-conversion.
- Thompson ([Thompson1991]), §2.3 "Evaluation," p. 36, Definition 2.8 — weak head normal form.
- Thompson ([Thompson1991]), §2.3 "Evaluation," p. 38, Theorem 2.10 — the Church–Rosser theorem.
- Mac Lane ([MacLane1998]), Ch. III §1 "Universal Arrows," p. 55 — the general categorical form of "universal property."
- Mac Lane ([MacLane1998]), Ch. I §5, p. 20 — initial object.
- Mac Lane ([MacLane1998]), Ch. I §3 "Functors," p. 14 — forgetful functor.
- Mac Lane ([MacLane1998]), Ch. III §7 "Subobjects and Generators," p. 126 — subobject. Equivalently, Pareigis ([Pareigis1970]), §1.6 "Subobjects and Quotient Objects," p. 20.
- Mac Lane ([MacLane1998]), Ch. I §3 "Functors," p. 15 — full subcategory.

[Pierce2002]: ../bibliography.md#pierce2002
[Thompson1991]: ../bibliography.md#thompson1991
[MacLane1998]: ../bibliography.md#maclane1998
[Pareigis1970]: ../bibliography.md#pareigis1970

---

[← Dependent types, with examples](03-dependent-types.md) | [Index](00-index.md) | [Next: Π/Σ-types and the calculus of constructions →](05-pi-sigma-and-coc.md)