Chapter 210Core route

Set-Level Mathematics in Univalent Foundations

Cardinals and ordinals

A cardinal remembers a set only up to equivalence. We obtain that quotient internally by taking the set truncation of the universe of sets.

Definition 74.48 — Cardinals ¶

The type of cardinals is $Card : = ‖ Set ‖_{0}$ ; a cardinal is therefore a set remembered only up to mere equivalence. The cardinality of a set $A$ is its class $| A | : Card$ . Arithmetic is defined by induction on $0$ -truncation: $| A | + | B | : = | A + B |, | A | \cdot | B | : = | A \times B |, | A |^{| B |} : = | B \to A | .$ To define addition, fix $A$ and eliminate the truncation in the second argument. For a representative $B$ , set $| A | + | B | : = | A + B |$ . The codomain $Card$ is a set, so the result is independent of the representative. Eliminate the first truncation in the same way. Products and exponentials are well defined by the same two eliminations, using $A \times B$ and $B \to A$ .

Referenced from 2 locations

Set-Level Mathematics in Univalent Foundations

Lemma 74.49 ¶

$(Card, 0, 1, +, \cdot)$ is a commutative semiring, with $0 : = | 0 |$ and $1 : = | 1 |$ . Moreover, $\begin{aligned} α^{0} & = 1, & α^{1} & = α, & α^{β + γ} & = α^{β} \cdot α^{γ}, \\ (α \cdot β)^{γ} & = α^{γ} \cdot β^{γ}, & α^{β \cdot γ} & = (α^{β})^{γ} . \end{aligned}$

Referenced from 4 locations

Proof of Lemma 74.49

Proof. Every asserted equality is a mere proposition, so truncation induction reduces it to representatives. The additive laws are induced by the equivalences $(A + B) + C ≃ A + (B + C), A + B ≃ B + A, 0 + A ≃ A .$ The multiplicative laws are induced by $(A \times B) \times C ≃ A \times (B \times C), A \times B ≃ B \times A, 1 \times A ≃ A, 0 \times A ≃ 0 .$ Distributivity is induced by $A \times (B + C) ≃ (A \times B) + (A \times C), (B + C) \times A ≃ (B \times A) + (C \times A) .$ Univalence turns each equivalence into the required cardinal equality. Finally, the displayed exponentiation laws are induced respectively by $(0 \to A) ≃ 1, (1 \to A) ≃ A, (B + C \to A) ≃ (B \to A) \times (C \to A),$ $C \to (A \times B) ≃ (C \to A) \times (C \to B), B \times C \to A ≃ C \to (B \to A) .$ ◻

Definition 74.50 ¶

For sets $A, B$ let $inj (A, B)$ be the type of injections $A \to B$ . Cardinal inequality is defined by truncation induction: $| A | \leq | B | : = ‖ inj (A, B) ‖$ .

Referenced from 2 locations

Set-Level Mathematics in Univalent Foundations

Theorem 74.51 — Cantor ¶

For any set $A$ there is no surjection $A \to (A \to 2)$ .

Referenced from 3 locations

Proof of Theorem 74.51 — Cantor

Proof. Let $f : A \to (A \to 2)$ and define $g (a) : = \neg f (a) (a)$ , with $\neg$ the Boolean negation. A surjection would merely provide $a_{0}$ with $f (a_{0}) = g$ ; applying both sides to $a_{0}$ gives $f (a_{0}) (a_{0}) = \neg f (a_{0}) (a_{0})$ , contradicting $tt \neq ff$ (theorem 29.14) after case analysis on $f (a_{0}) (a_{0})$ . Since $0$ is a mere proposition, mere existence suffices for the contradiction. ◻

Theorem 74.52 — Schr"oder–Bernstein; LEM ¶

Assuming the law of excluded middle for mere propositions, for sets $A, B$ there is a map $inj (A, B) \to inj (B, A) \to (A ≅ B)$ ; hence, assuming LEM, $\leq$ on $Card$ is a partial order.

Referenced from 2 locations

Set-Level Mathematics in Univalent Foundations

Proof of Theorem 74.52 — Schr"oder–Bernstein; LEM

Proof. Let $f : A \to B$ and $g : B \to A$ be injections. Define subsets of $A$ by $C_{0} : = A ∖ im (g), q q u a d C_{n + 1} : = g (f (C_{n})), q q u a d C : = ⋃_{n : N} C_{n} .$ Membership in each subset is a mere proposition, and LEM decides membership in $C$ . If $a \in C$ , put $h (a) : = f (a)$ . If $a \notin C$ , then $a \notin C_{0}$ , so there is a unique $b : B$ with $g (b) = a$ ; put $h (a) : = b$ .

Suppose $h (a) = h (a^{'})$ . If $a, a^{'} \in C$ , injectivity of $f$ gives $a = a^{'}$ . If neither lies in $C$ , applying $g$ to the equality gives $a = a^{'}$ . In the remaining case, say $a \in C_{n}$ and $a^{'} \notin C$ , the equality $f (a) = h (a^{'})$ gives $a^{'} = g (f (a)) \in C_{n + 1}$ , a contradiction. Thus $h$ is injective.

For surjectivity, take $b : B$ . If $g (b) \notin C$ , the unique inverse clause gives $h (g (b)) = b$ . If $g (b) \in C$ , then $g (b) \notin C_{0}$ and its membership witness has successor form: $g (b) = g (f (a))$ for some $a \in C_{n}$ . Injectivity of $g$ gives $b = f (a) = h (a)$ . Hence $h : A ≅ B$ .

Reflexivity and transitivity of cardinal inequality come from identity and composition of injections. Given both $| A | \leq | B |$ and $| B | \leq | A |$ , eliminate the two propositional truncations into the proposition $| A | = | B |$ , apply the construction above, and use univalence. Thus $\leq$ is antisymmetric. ◻

Definition 74.53 — Accessibility ¶

Let $A$ be a set with a mere relation $< : A \to A \to Prop$ . The family $acc : A \to U$ is inductively generated by the single rule

Γ ⊢ a : A

Γ ⊢ h : \prod_{b : A} (b < a) \to acc (b)

Γ ⊢ {acc}_{<} (a, h) : acc (a)

Acc-Intro

with the corresponding induction principle for an indexed inductive family (cf. chapter 28). An inhabitant of $acc (a)$ is an accessibility witness: it contains accessibility witnesses for every predecessor of $a$ . The relation $<$ is well-founded if $\prod_{a : A} acc (a)$ .

Referenced from 2 locations

Set-Level Mathematics in Univalent Foundations

Lemma 74.54 ¶

Each $acc (a)$ is a mere proposition; hence well-foundedness is a mere proposition.

Referenced from 3 locations

Set-Level Mathematics in Univalent Foundations

Proof of Lemma 74.54

Proof. Fix $a$ and an accessibility witness $u : acc (a)$ . Induct on $u$ with motive $P (a, u) : = \prod_{v : acc (a)} u = v .$ In the constructor case $u = {acc}_{<} (a, h_{1})$ , take $v = {acc}_{<} (a, h_{2})$ . For every $b : A$ and $r : b < a$ , the induction hypothesis at $h_{1} (b, r)$ gives $h_{1} (b, r) = h_{2} (b, r)$ . Function extensionality first in $r$ and then in $b$ gives $h_{1} = h_{2}$ . Congruence of ${acc}_{<} (a, -)$ therefore gives $u = v$ . Hence every two witnesses of $acc (a)$ are equal. A dependent product of mere propositions is a mere proposition, so well-foundedness is one as well. ◻

Theorem 74.55 — Well-founded induction ¶

Let $<$ be well-founded on $A$ and $P : A \to U$ . If $\prod_{a : A} (\prod_{b : A} (b < a) \to P (b)) \to P (a)$ , then $\prod_{a : A} P (a)$ .

Referenced from 2 locations

Set-Level Mathematics in Univalent Foundations

Proof of Theorem 74.55 — Well-founded induction

Proof. By $acc$ -induction $P$ holds at every accessible element, and well-foundedness makes every element accessible. ◻

Definition 74.56 — Ordinals ¶

A well-founded mere relation $<$ on a set $A$ is extensional if $\prod_{a : A} \prod_{b : A} (\prod_{c : A} (c < a) \leftrightarrow (c < b)) \to (a = b) .$ An ordinal is a set with an extensional, well-founded, transitive mere relation; $Ord$ denotes the type of ordinals in $U$ .

Referenced from 2 locations

Set-Level Mathematics in Univalent Foundations

Theorem 74.57 ¶

The type of sets equipped with extensional well-founded relations is a set; in particular $Ord$ is a set.

Referenced from 2 locations

Set-Level Mathematics in Univalent Foundations

Proof of Theorem 74.57

Proof. By univalence and the machinery of theorem 74.44 it suffices to show that the only automorphism $f$ of an extensional well-founded $(A, <)$ is the identity. By well-founded induction suppose $f (a^{'}) = a^{'}$ for all $a^{'} < a$ . For $c < a$ we get $f (c) = c$ , so $c < f (a)$ (as $f$ preserves $<$ ). Conversely, if $c < f (a)$ , preservation by $f^{- 1}$ gives $f^{- 1} (c) < a$ . The induction hypothesis gives $f^{- 1} (c) = c$ , hence $c < a$ . Thus $a$ and $f (a)$ have the same predecessors, so extensionality gives $f (a) = a$ . ◻

Definition 74.58 — Simulation ¶

For ordinals $(A, <)$ , $(B, <)$ , a simulation is a map $f : A \to B$ such that (i) $a < a^{'}$ implies $f (a) < f (a^{'})$ , and (ii) whenever $b < f (a)$ there merely exists $a^{'} < a$ with $f (a^{'}) = b$ . We write $A \leq B$ for the mere proposition that one exists, and $A < B$ if some simulation identifies $A$ with an initial segment ${b^{'} : B ∣ b^{'} < b}$ of $B$ .

Referenced from 2 locations

Set-Level Mathematics in Univalent Foundations

Lemma 210.12 — Uniqueness of simulations ¶

A simulation between two ordinals is injective, and any two simulations $f, g : A \to B$ are equal. If simulations exist in both directions, they form an isomorphism of the underlying extensional well-founded relations.

Referenced from 4 locations

Set-Level Mathematics in Univalent Foundations

Proof of Lemma 210.12 — Uniqueness of simulations

Proof. Fix a simulation $f : A \to B$ . Prove by well-founded induction on $a : A$ the strengthened motive $P (a) : = \prod_{a^{'} : A} (f (a) = f (a^{'})) \to (a = a^{'}) .$ Suppose $f (a) = f (a^{'})$ . If $c < a$ , then $f (c) < f (a^{'})$ ; the initial-segment clause at $a^{'}$ gives, under propositional truncation, $c^{'} < a^{'}$ with $f (c^{'}) = f (c)$ . The target $c = c^{'}$ is a mere proposition, so eliminate the truncation and apply the induction hypothesis $P (c)$ to obtain it. Conversely, if $c^{'} < a^{'}$ , the same clause at $a$ gives $c < a$ with $f (c) = f (c^{'})$ , and $P (c)$ again gives $c = c^{'}$ . Thus $a$ and $a^{'}$ have the same predecessors. Extensionality of $A$ gives $a = a^{'}$ , completing the induction and proving that $f$ is injective.

For uniqueness, induct on $a : A$ . If $b < f (a)$ , the initial-segment clause gives $a^{'} < a$ with $f (a^{'}) = b$ . The induction hypothesis gives $f (a^{'}) = g (a^{'})$ , so $b < g (a)$ . The converse is symmetric. Extensionality of $B$ yields $f (a) = g (a)$ , and function extensionality gives $f = g$ .

Given $f : A \to B$ and $g : B \to A$ , both $g \circ f$ and ${id}_{A}$ are simulations; uniqueness in $A$ gives $g \circ f = {id}_{A}$ . Both $f \circ g$ and ${id}_{B}$ are simulations, so uniqueness in $B$ gives $f \circ g = {id}_{B}$ . Hence $f$ and $g$ are inverse isomorphisms preserving the relations. ◻

Theorem 74.59 ¶

$({Ord}_{U}, <)$ is an ordinal in the next universe.

Referenced from 2 locations

Set-Level Mathematics in Univalent Foundations

Proof of Theorem 74.59

Proof. Write $A ↓ a$ for the ordinal on ${a^{'} : A ∣ a^{'} < a}$ .

Transitivity. Suppose $A < B$ is represented by a simulation identifying $A$ with $B ↓ b$ , and $B < C$ by one identifying $B$ with $C ↓ c$ . Their composite identifies $A$ with $C ↓ f (b)$ , where $f (b) < c$ ; hence $A < C$ .

Extensionality. Suppose $X < A$ if and only if $X < B$ for every small ordinal $X$ . For each $a : A$ , the relation $A ↓ a < A$ gives a unique $b : B$ such that $A ↓ a = B ↓ b .$ Uniqueness follows from extensionality of $B$ , so propositional elimination defines $f (a) : = b$ . If $a^{'} < a$ , then $A ↓ a^{'} < A ↓ a$ ; transporting across the displayed equalities gives $f (a^{'}) < f (a)$ . Conversely, every $b^{'} < f (a)$ determines the predecessor ordinal $B ↓ b^{'} < B ↓ f (a)$ and therefore a unique $a^{'} < a$ with $f (a^{'}) = b^{'}$ . Thus $f : A \to B$ is a simulation. The symmetric construction gives a simulation $B \to A$ , so lemma 210.12 and the structure identity principle give $A = B$ .

Well-foundedness. Fix $A$ and prove $acc (A ↓ a)$ by well-founded induction on $a : A$ . The proposition $X < A ↓ a$ is, by definition, the truncation of a pair $u : (A ↓ a)$ and a relation isomorphism $X ≅ (A ↓ a) ↓ u$ . Write $u = (a^{'}, r)$ , where $r : a^{'} < a$ . There is a relation isomorphism $(A ↓ a) ↓ (a^{'}, r) ≅ A ↓ a^{'}$ whose forward map sends $((b, s), t)$ to $(b, t)$ and whose inverse sends $(b, t)$ to $((b, trans (t, r)), t)$ . The structure identity principle therefore gives $X = A ↓ a^{'}$ . Because accessibility is a mere proposition, we may eliminate the truncation; the induction hypothesis at $a^{'} < a$ then gives $acc (X)$ . Hence Acc-Intro gives $acc (A ↓ a)$ .

Finally, an element of $X < A$ is exactly a truncated pair of $a : A$ and a relation isomorphism $X ≅ A ↓ a$ . Eliminate it into the proposition $acc (X)$ and use the result just proved. One more use of Acc-Intro gives $acc (A)$ . Thus the relation on ${Ord}_{U}$ is well founded. Its carrier belongs to the next universe by construction. ◻

No Burali–Forti contradiction follows. The type ${Ord}_{U}$ belongs to the next universe, and the assignment $A \mapsto {B ∣ B < A}$ does not lower that universe level.

Exercise 74.14 ¶

★★★ For each equivalence used in lemma 74.49, write its inverse and verify both composites. Then show that $\leq$ is compatible with $+$ and $\cdot$ , and that exponentiation is monotone in its base: $α \leq β$ implies $α^{γ} \leq β^{γ}$ .

Referenced from 3 locations

Exercise 74.15 ¶

★★☆ Write out the proof of lemma 74.54, using the induction principle of $acc$ with a motive depending on the accessibility witness.

Referenced from 3 locations

Exercise 74.16 ¶

★★★ Reconstruct lemma 210.12. Identify where well-founded induction is used for injectivity and where extensionality is used for uniqueness.

Referenced from 3 locations

Suggested first pass.

None of these problems is a prerequisite for a later chapter. Begin with exercise 210.4, then complete exercise 210.5.

Exercise 210.4 ¶

★★☆ Let $e : A \to (A \to 2)$ be arbitrary and define $d (a) : = not (e (a) (a))$ . Prove that no $a : A$ satisfies $e (a) = d$ , and conclude that no map $A \to (A \to 2)$ is surjective. State precisely where function congruence and Boolean separation enter the argument, and explain why excluded middle is not used.

Referenced from 4 locations

Exercise 210.5 ¶

★★★ Practical project.finite-cardinal-evaluator Implement in Agda or Kappa a finite evaluator for cardinal expressions built from $0$ , $1$ , natural-number constants, sum, product, and exponentiation. Check a sum, distributivity, $(a^{b})^{c} = a^{b c}$ , and the finite Cantor inequality $n < 2^{n}$ on named inputs. Mutation test: replace the sum clause by its left operand; the sum or distributivity acceptance test must then fail. The program tests finite representatives only and must not claim to decide equality of arbitrary cardinals.

Referenced from 5 locations

Bibliographic notes

The set-level and ordinal developments follow Chapter 10 of the HoTT Book [Uni13]. In particular, ordinals are sets with extensional, well-founded, transitive relations, and the type of small ordinals is itself an ordinal one universe higher. None of the cardinal or ordinal constructions depends on the optional real-number completion.