10.3 Ordinal numbers

Definition 10.3.1.

Let $A$ be a set and

a binary relation on $A$.We define by induction what it means for an element $a\mathrm{:}A$ to be accessibleby :

• If $b$ is accessible for every , then $a$ is accessible.

We write $\mathrm{acc}\mathit{}\mathrm{(}a\mathrm{)}$ to mean that $a$ is accessible.

It may seem that such an inductive definition can never get off the ground, but of course if $a$ has the property that there are no $b$ such that , then $a$ is vacuously accessible.

Note that this is an inductive definition of a family of types, like the type of vectors considered in sec:generalizations.More precisely, it has one constructor, say , with type

The induction principle for $\mathrm{𝖺𝖼𝖼}$ says that for any $P:{\prod }_{(a:A)}\mathrm{𝖺𝖼𝖼}(a)\to 𝒰$, if we have

then we have $g:{\prod }_{(a:A)}{\prod }_{(c:\mathrm{𝖺𝖼𝖼}(a))}P(a,c)$ defined by induction, with

This is a mouthful, but generally we apply it only in the simpler case where $P:A\to 𝒰$ depends only on $A$.In this case the second and third arguments of $f$ may be combined, so that what we have to prove is

That is, we assume every is accessible and $g(b):P(b)$ is defined, and from these define $g(a):P(a)$.

The omission of the second argument of $P$ is justified by the following lemma, whose proof is the only place where we use the more general form of the induction principle.

Lemma 10.3.2.

Accessibility is a mere property.

Proof.

We must show that for any $a:A$ and $s_1,s_2:\mathrm{𝖺𝖼𝖼}(a)$ we have $s_1=s_2$.We prove this by induction on $s_1$, with

$$P_1(a,s_1):\equiv \prod _{s_2:\mathrm{𝖺𝖼𝖼}(a)}(s_1=s_2).$$

Thus, we must show that for any $a:A$ and and

we have for any $s_2:\mathrm{𝖺𝖼𝖼}(a)$.We regard this statement as ${\prod }_{(a:A)}{\prod }_{(s_2:\mathrm{𝖺𝖼𝖼}(a))}{P}_2(a,s_2)$, where

thus we may prove it by induction on $s_2$.Therefore, we assume , and $k_2$ with a monstrous but irrelevant type,and must show that for any $h_1$ and $k_1$ with types as above,we have .By function extensionality, it suffices to show $h_1(b,l)=h_2(b,l)$ for all $b:A$ and .This follows from $k_1$.∎

Definition 10.3.3.

A binary relation on a set $A$ is well-foundedif every element of $A$ is accessible.

The point of well-foundedness is that for $P:A\to 𝒰$, we can use the induction principle of $\mathrm{𝖺𝖼𝖼}$ to conclude ${\prod }_{(a:A)}\mathrm{𝖺𝖼𝖼}(a)\to P(a)$, and then apply well-foundedness to conclude ${\prod }_{(a:A)}P(a)$.In other words, if from we can prove $P(a)$, then $\forall (a:A).P(a)$.This is called well-founded induction.

Lemma 10.3.4.

Well-foundedness is a mere property.

Proof.

Well-foundedness of is the type ${\prod }_{(a:A)}\mathrm{𝖺𝖼𝖼}(a)$, which is a mere proposition since each $\mathrm{𝖺𝖼𝖼}(a)$ is.∎

Example 10.3.5.

Perhaps the most familiar well-founded relation is the usual strict ordering on $\mathrm{N}$.To show that this is well-founded, we must show that $n$ is accessible for each $n\mathrm{:}\mathrm{N}$.This is just the usual proof of “strong induction” from ordinary induction on $\mathrm{N}$.

Specifically, we prove by induction on $n\mathrm{:}\mathrm{N}$ that $k$ is accessible for all $k\mathrm{\le }n$.The base case is just that $\mathrm{0}$ is accessible, which is vacuously true since nothing is strictly less than $\mathrm{0}$.For the inductive step, we assume that $k$ is accessible for all $k\mathrm{\le }n$, which is to say for all ; hence by definition $n\mathrm{+}\mathrm{1}$ is also accessible.

A different relation on $\mathrm{N}$ which is also well-founded is obtained by setting only for all $n\mathrm{:}\mathrm{N}$.Well-foundedness of this relation is almost exactly the ordinary induction principle of $\mathrm{N}$.

Example 10.3.6.

Let $A\mathrm{:}$ and $B\mathrm{:}A\mathrm{\to }$ be a family of sets.Recall from sec:w-types that the $W$-type ${\mathrm{W}}_{\mathrm{(}a\mathrm{:}A\mathrm{)}}\mathit{}B\mathit{}\mathrm{(}a\mathrm{)}$ is inductively generated by the single constructor

• $\mathrm{𝗌𝗎𝗉}:{\prod }_{(a:A)}(B(a)\to {𝖶}_{(x:A)}B(x))\to {𝖶}_{(x:A)}B(x)$

We define the relation on ${\mathrm{W}}_{\mathrm{(}x\mathrm{:}A\mathrm{)}}\mathit{}B\mathit{}\mathrm{(}x\mathrm{)}$ by recursion on its second argument:

• For any $a:A$ and $f:B(a)\to {𝖶}_{(x:A)}B(x)$, we define to mean that there merely exists a $b:B(a)$ such that $w=f(b)$.

Now we prove that every $w\mathrm{:}{\mathrm{W}}_{\mathrm{(}x\mathrm{:}A\mathrm{)}}\mathit{}B\mathit{}\mathrm{(}x\mathrm{)}$ is accessible for this relation, using the usual induction principle for ${\mathrm{W}}_{\mathrm{(}x\mathrm{:}A\mathrm{)}}\mathit{}B\mathit{}\mathrm{(}x\mathrm{)}$.This means we assume given $a\mathrm{:}A$ and $f\mathrm{:}B\mathit{}\mathrm{(}a\mathrm{)}\mathrm{\to }{\mathrm{W}}_{\mathrm{(}x\mathrm{:}A\mathrm{)}}\mathit{}B\mathit{}\mathrm{(}x\mathrm{)}$, and also a lifting $f^{\mathrm{\prime }}\mathrm{:}{\mathrm{\prod }}_{\mathrm{(}b\mathrm{:}B\mathrm{(}a\mathrm{)}\mathrm{)}}\mathrm{acc}\mathit{}\mathrm{(}f\mathit{}\mathrm{(}b\mathrm{)}\mathrm{)}$.But then by definition of , we have $\mathrm{acc}\mathit{}\mathrm{(}w\mathrm{)}$ for all ; hence $\sup \mathit{}\mathrm{(}a\mathrm{,}f\mathrm{)}$ is accessible.

Well-foundedness allows us to define functions by recursion and prove statements by induction, such as for instance the following.Recall from subsec:prop-subsets that $𝒫(B)$ denotes the power set $𝒫(B):\equiv (B\to \mathrm{𝖯𝗋𝗈𝗉})$.

Lemma 10.3.7.

Suppose $B$ is a set and we have a function

$$g:𝒫(B)\to B$$

Then if is a well-founded relation on $A$, there is a function $f\mathrm{:}A\mathrm{\to }B$ such that for all $a\mathrm{:}A$ we have

(We are using the notation for images of subsets from sec:image.)

Proof.

We first define, for every $a:A$ and $s:\mathrm{𝖺𝖼𝖼}(a)$, an element $\overline{f}(a,s):B$.By induction, it suffices to assume that $s$ is a function assigning to each a witness $s(a^{\prime }):\mathrm{𝖺𝖼𝖼}(a^{\prime })$, and that moreover for each such $a^{\prime }$ we have an element $\overline{f}(a^{\prime },s(a^{\prime })):B$.In this case, we define

Now since is well-founded, we have a function $w:{\prod }_{(a:A)}\mathrm{𝖺𝖼𝖼}(a)$.Thus, we can define $f(a):\equiv \overline{f}(a,w(a))$.∎

In classical logic, well-foundedness has a more well-known reformulation.In the following, we say that a subset $B:𝒫(A)$ is nonemptyif it is unequal to the empty subset $(\lambda x.\perp ):𝒫(X)$.We leave it to the reader to verify that assuming excluded middle, this is equivalent to mere inhabitation, i.e. to the condition $\exists (x:A).x\in B$.

Lemma 10.3.8.

Assuming excluded middle, is well-founded if and only if every nonempty subset $B\mathrm{:}\mathrm{P}\mathit{}\mathrm{(}A\mathrm{)}$ merely has a minimal element.

Proof.

Suppose first is well-founded, and suppose $B\subseteq A$ is a subset with no minimal element.That is, for any $a:A$ with $a\in B$, there merely exists a $b:A$ with and $b\in B$.

We claim that for any $a:A$ and $s:\mathrm{𝖺𝖼𝖼}(a)$, we have $a\notin B$.By induction, we may assume $s$ is a function assigning to each a proof $s(a^{\prime }):\mathrm{𝖺𝖼𝖼}(a)$, and that moreover for each such $a^{\prime }$ we have $a^{\prime }\notin B$.If $a\in B$, then by assumption, there would merely exist a with $b\in B$, which contradicts this assumption.Thus, $a\notin B$; this completes the induction.Since is well-founded, we have $a\notin B$ for all $a:A$, i.e. $B$ is empty.

Now suppose each nonempty subset merely has a minimal element.Let $B=a:A|\mathrm{\neg }\mathrm{𝖺𝖼𝖼}(a)$.Then if $B$ is nonempty, it merely has a minimal element.Thus there merely exists an $a:A$ with $a\in B$ such that for all , we have $\mathrm{𝖺𝖼𝖼}(b)$.But then by definition (and induction on truncation), $a$ is merely accessible, and hence accessible, contradicting $a\in B$.Thus, $B$ is empty, so is well-founded.∎

Definition 10.3.9.

A well-founded relation on a set $A$ is extensionalif for any $a\mathrm{,}b\mathrm{:}A$, we have

Note that since $A$ is a set, extensionality is a mere proposition.This notion of “extensionality” is unrelated to function extensionality, and also unrelated to the extensionality of identity types.Rather, it is a “local” counterpart of the axiom of extensionality in classical set theory.

Theorem 10.3.10.

The type of extensional well-founded relations is a set.

Proof.

By the univalence axiom, it suffices to show that if is extensional and well-founded and , then $f={\mathrm{𝗂𝖽}}_A$.We prove by induction on that $f(a)=a$ for all $a:A$.The inductive hypothesis is that for all , we have $f(a^{\prime })=a^{\prime }$.

Now since $A$ is extensional, to conclude $f(a)=a$ it is sufficient to show

However, since $f$ is an automorphism, we have .But implies $f(c)=c$ by the inductive hypothesis, so .On the other hand, if , then , and so $c=f(f^{-1}(c))=f^{-1}(c)$ by the inductive hypothesis again; thus .Therefore, we have for any $c:A$, so $f(a)=a$.∎

Definition 10.3.11.

If and are extensional and well-founded, a simulationis a function $f\mathrm{:}A\mathrm{\to }B$ such that

1. if , then , and

2. for all $a:A$ and $b:B$, if , then there merely exists an with $f(a^{\prime })=b$.

Lemma 10.3.12.

Any simulation is injective.

Proof.

We prove by double well-founded induction that for any $a,b:A$, if $f(a)=f(b)$ then $a=b$.The inductive hypothesis for $a:A$ says that for any , and any $b:B$, if $f(a^{\prime })=f(b)$ then $a=b$.The inner inductive hypothesis for $b:A$ says that for any , if $f(a)=f(b^{\prime })$ then $a=b^{\prime }$.

Suppose $f(a)=f(b)$; we must show $a=b$.By extensionality, it suffices to show that for any $c:A$ we have .If , then by def:simulation1.Hence , so by def:simulation2 there merely exists $c^{\prime }:A$ with and $f(c)=f(c^{\prime })$.By the inductive hypothesis for $a$, we have $c=c^{\prime }$, hence .The dual argument is symmetrical.∎

In particular, this implies that in def:simulation2 the word “merely” could be omitted without change of sense.

Corollary 10.3.13.

If $f\mathrm{:}A\mathrm{\to }B$ is a simulation, then for all $a\mathrm{:}A$ and $b\mathrm{:}B$, if , there purely exists an with $f\mathit{}\mathrm{(}{a}^{\mathrm{\prime }}\mathrm{)}\mathrm{=}b$.

Proof.

Since $f$ is injective, ${\sum }_{(a:A)}(f(a)=b)$ is a mere proposition.∎

We say that a subset $C:𝒫(B)$ is an initial segmentif $c\in C$ and imply $b\in C$.The image of a simulation must be an initial segment, while the inclusion of any initial segment is a simulation.Thus, by univalence, every simulation $A\to B$ is equal to the inclusion of some initial segment of $B$.

Theorem 10.3.14.

For a set $A$, let $P\mathit{}\mathrm{(}A\mathrm{)}$ be the type of extensional well-founded relations on $A$.If and and $f\mathrm{:}A\mathrm{\to }B$, let be the mere proposition that $f$ is a simulation.Then $\mathrm{(}P\mathrm{,}H\mathrm{)}$ is a standard notion of structure over $\mathrm{S}\mathit{}e\mathit{}t$ in the sense of sec:sip.

Proof.

We leave it to the reader to verify that identities are simulations, and that composites of simulations are simulations.Thus, we have a notion of structure.For standardness, we must show that if and $\prec$ are two extensional well-founded relations on $A$, and ${\mathrm{𝗂𝖽}}_A$ is a simulation in both directions, then and $\prec$ are equal.Since extensionality and well-foundedness are mere propositions, for this it suffices to have .But this follows from def:simulation1 for ${\mathrm{𝗂𝖽}}_A$.∎

Corollary 10.3.15.

There is a category whose objects are sets equipped with extensional well-founded relations, and whose morphisms are simulations.

In fact, this category is a poset.

Lemma 10.3.16.

For extensional and well-founded and , there is at most one simulation $f\mathrm{:}A\mathrm{\to }B$.

Proof.

Suppose $f,g:A\to B$ are simulations.Since being a simulation is a mere property, it suffices to show $\forall (a:A).(f(a)=g(a))$.By induction on , we may suppose $f(a^{\prime })=g(a^{\prime })$ for all .And by extensionality of $B$, to have $f(a)=g(a)$ it suffices to have .

But since $f$ is a simulation, if , then we have with $f(a^{\prime })=b$.By the inductive hypothesis, we have also $g(a^{\prime })=b$, hence .The dual argument is symmetrical.∎

Thus, if $A$ and $B$ are equipped with extensional and well-founded relations, we may write $A\le B$ to mean there exists a simulation $f:A\to B$.thm:wfcat implies that if $A\le B$ and $B\le A$, then $A=B$.

Definition 10.3.17.

An ordinalis a set $A$ with an extensional well-founded relation which is transitive, i.e. satisfies .

Example 10.3.18.

Of course, the usual strict order on $\mathrm{N}$ is transitive.It is easily seen to be extensional as well; thus it is an ordinal.As usual, we denote this ordinal by $\omega$.

Let $\mathrm{𝖮𝗋𝖽}$ denote the type of ordinals.By the previous results, $\mathrm{𝖮𝗋𝖽}$ is a set and has a natural partial order.We now show that $\mathrm{𝖮𝗋𝖽}$ also admits a well-founded relation.

If $A$ is an ordinal and $a:A$, let denote the initial segment.Note that if $A_{/a}=A_{/b}$ as ordinals, then that isomorphism must respect their inclusions into $A$ (since simulations form a poset), and hence they are equal as subsets of $A$.Therefore, since $A$ is extensional, $a=b$.Thus the function $a\mapsto A_{/a}$ is an injection $A\to \mathrm{𝖮𝗋𝖽}$.

Definition 10.3.19.

For ordinals $A$ and $B$, a simulation $f\mathrm{:}A\mathrm{\to }B$ is said to be boundedif there exists $b\mathrm{:}B$ such that $A\mathrm{=}{B}_{\mathrm{/}b}$.

The remarks above imply that such a $b$ is unique when it exists, so that boundedness is a mere property.

We write if there exists a bounded simulation from $A$ to $B$.Since simulations are unique, is also a mere proposition.

Theorem 10.3.20.

is an ordinal.

More precisely, this theorem says that the type ${\mathrm{𝖮𝗋𝖽}}_{{𝒰}_i}$ of ordinals in one universe is itself an ordinal in the next higher universe, i.e. .

Proof.

Let $A$ be an ordinal; we first show that $A_{/a}$ is accessible (in $\mathrm{𝖮𝗋𝖽}$) for all $a:A$.By well-founded induction on $A$, suppose $A_{/b}$ is accessible for all .By definition of accessibility, we must show that $B$ is accessible in $\mathrm{𝖮𝗋𝖽}$ for all .However, if then there is some such that $B={(A_{/a})}_{/b}=A_{/b}$, which is accessible by the inductive hypothesis.Thus, $A_{/a}$ is accessible for all $a:A$.

Now to show that $A$ is accessible in $\mathrm{𝖮𝗋𝖽}$, by definition we must show $B$ is accessible for all .But as before, means $B=A_{/a}$ for some $a:A$, which is accessible as we just proved.Thus, $\mathrm{𝖮𝗋𝖽}$ is well-founded.

For extensionality, suppose $A$ and $B$ are ordinals such thatThen for every $a:A$, since , we have , hence there is $b:B$ with $A_{/a}=B_{/b}$.Define $f:A\to B$ to take each $a$ to the corresponding $b$; it is straightforward to verify that $f$ is an isomorphism.Thus $A\cong B$, hence $A=B$ by univalence.

Finally, it is easy to see that is transitive.∎

Treating $\mathrm{𝖮𝗋𝖽}$ as an ordinal is often very convenient, but it has its pitfalls as well.For instance, consider the following lemma, where we pay attention to how universes are used.

Lemma 10.3.21.

Let $\mathrm{U}$ be a universe.For any $A\mathrm{:}{\mathrm{Ord}}_{\mathrm{U}}$, there is a $B\mathrm{:}{\mathrm{Ord}}_{\mathrm{U}}$ such that .

Proof.

Let $B=A+\mathrm{𝟏}$, with the element $\star :\mathrm{𝟏}$ being greater than all elements of $A$.Then $B$ is an ordinal and it is easy to see that $A\cong B_{/\star }$.∎

This lemma illustrates a potential pitfall of the “typically ambiguous” style of using $𝒰$ to denote an arbitrary, unspecified universe.Consider the following alternative proof of it.

Another putative proof of thm:ordsucc.

Note that if and only if $C=A_{/a}$ for some $a:A$.This gives an isomorphism $A\cong {\mathrm{𝖮𝗋𝖽}}_{/A}$, so that .Thus we may take $B:\equiv \mathrm{𝖮𝗋𝖽}$.∎

The second proof would be valid if we had stated thm:ordsucc in a typically ambiguous style.But the resulting lemma would be less useful, because the second proof would constrain the second “$\mathrm{𝖮𝗋𝖽}$” in the lemma statement to refer to a higher universe level than the first one.The first proof allows both universes to be the same.

Similar remarks apply to the next lemma, which could be proved in a less useful way by observing that $A\le \mathrm{𝖮𝗋𝖽}$ for any $A:\mathrm{𝖮𝗋𝖽}$.

Lemma 10.3.22.

Let $\mathrm{U}$ be a universe.For any $X\mathrm{:}\mathrm{U}$ and $F\mathrm{:}X\mathrm{\to }{\mathrm{Ord}}_{\mathrm{U}}$, there exists $B\mathrm{:}{\mathrm{Ord}}_{\mathrm{U}}$ such that $F\mathit{}x\mathrm{\le }B$ for all $x\mathrm{:}X$.

Proof.

Let $B$ be the quotient of the equivalence relation $\sim$ on ${\sum }_{(x:X)}Fx$ defined as follows:

$$(x,y)\sim (x^{\prime },y^{\prime }):\equiv ({(Fx)}_{/y}\cong {(F{x}^{\prime })}_{/y^{\prime }}).$$

Define if .This clearly descends to the quotient, and can be seen to make $B$ into an ordinal.Moreover, for each $x:X$ the induced map $Fx\to B$ is a simulation.∎