10.3 Ordinal numbers

Definition 10.3.1.

Let A be a set and


a binary relationMathworldPlanetmath on A. We define by inductionMathworldPlanetmath what it means for an element a:A to be accessiblePlanetmathPlanetmath by <:

  • โ€ข

    If b is accessible for every b<a, then a is accessible.

We write accโข(a) 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 b<a, then a is vacuously accessible.

Note that this is an inductive definition of a family of types, like the type of vectors considered in \autorefsec:generalizationsPlanetmathPlanetmath. More precisely, it has one constructor, say ๐–บ๐–ผ๐–ผ<, with type


The induction principle for ๐–บ๐–ผ๐–ผ says that for any P:โˆ(a:A)๐–บ๐–ผ๐–ผโข(a)โ†’๐’ฐ, if we have


then we have g:โˆ(a:A)โˆ(c:๐–บ๐–ผ๐–ผ(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โ†’๐’ฐ 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 b<a 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.


We must show that for any a:A and s1,s2:๐–บ๐–ผ๐–ผโข(a) we have s1=s2. We prove this by induction on s1, with


Thus, we must show that for any a:A and h1:โˆ(b:A)(b<a)โ†’๐–บ๐–ผ๐–ผ(b) and


we have ๐–บ๐–ผ๐–ผ<โข(a,h)=s2 for any s2:๐–บ๐–ผ๐–ผโข(a). We regard this statement as โˆ(a:A)โˆ(s2:๐–บ๐–ผ๐–ผ(a))P2โข(a,s2), where


thus we may prove it by induction on s2. Therefore, we assume h2:โˆ(b:A)(b<a)โ†’๐–บ๐–ผ๐–ผ(b), and k2 with a monstrous but irrelevant type, and must show that for any h1 and k1 with types as above, we have ๐–บ๐–ผ๐–ผ<โข(a,h1)=๐–บ๐–ผ๐–ผ<โข(a,h2). By function extensionality, it suffices to show h1โข(b,l)=h2โข(b,l) for all b:A and l:b<a. This follows from k1. โˆŽ

Definition 10.3.3.

A binary relation < on a set A is well-founded if every element of A is accessible.

The point of well-foundedness is that for P:Aโ†’๐’ฐ, we can use the induction principle of ๐–บ๐–ผ๐–ผ to conclude โˆ(a:A)๐–บ๐–ผ๐–ผโข(a)โ†’Pโข(a), and then apply well-foundedness to conclude โˆ(a:A)Pโข(a). In other words, if from โˆ€(b:A).(b<a)โ†’P(b) we can prove Pโข(a), then โˆ€(a:A).P(a). This is called well-founded induction.

Lemma 10.3.4.

Well-foundedness is a mere property.


Well-foundedness of < is the type โˆ(a:A)๐–บ๐–ผ๐–ผโข(a), which is a mere proposition since each ๐–บ๐–ผ๐–ผโข(a) is. โˆŽ

Example 10.3.5.

Perhaps the most familiar well-founded relation is the usual strict ordering on N. To show that this is well-founded, we must show that n is accessible for each n:N. This is just the usual proof of โ€œstrong inductionโ€ from ordinary induction on N.

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

A different relation on N which is also well-founded is obtained by setting only n<succโข(n) for all n:N. Well-foundedness of this relationMathworldPlanetmath is almost exactly the ordinary induction principle of N.

Example 10.3.6.

Let A:\set and B:Aโ†’\set be a family of sets. Recall from \autorefsec:w-types that the W-type W(a:A)โขBโข(a) is inductively generated by the single constructor

  • โ€ข


We define the relation < on W(x:A)โขBโข(x) by recursion on its second argument:

  • โ€ข

    For any a:A and f:Bโข(a)โ†’๐–ถ(x:A)โขBโข(x), we define w<๐—Œ๐—Ž๐—‰โข(a,f) to mean that there merely exists a b:Bโข(a) such that w=fโข(b).

Now we prove that every w:W(x:A)โขBโข(x) is accessible for this relation, using the usual induction principle for W(x:A)โขBโข(x). This means we assume given a:A and f:Bโข(a)โ†’W(x:A)โขBโข(x), and also a lifting fโ€ฒ:โˆ(b:B(a))accโข(fโข(b)). But then by definition of <, we have accโข(w) for all w<supโข(a,f); hence supโข(a,f) is accessible.

Well-foundedness allows us to define functions by recursion and prove statements by induction, such as for instance the following. Recall from \autorefsubsec:prop-subsets that ๐’ซโข(B) denotes the power setMathworldPlanetmath ๐’ซ(B):โ‰ก(Bโ†’๐–ฏ๐—‹๐—ˆ๐—‰).

Lemma 10.3.7.

Suppose B is a set and we have a function


Then if < is a well-founded relation on A, there is a function f:Aโ†’B such that for all a:A we have


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


We first define, for every a:A and s:๐–บ๐–ผ๐–ผโข(a), an element fยฏโข(a,s):B. By induction, it suffices to assume that s is a function assigning to each aโ€ฒ<a a witness sโข(aโ€ฒ):๐–บ๐–ผ๐–ผโข(aโ€ฒ), and that moreover for each such aโ€ฒ we have an element fยฏโข(aโ€ฒ,sโข(aโ€ฒ)):B. In this case, we define


Now since < is well-founded, we have a function w:โˆ(a:A)๐–บ๐–ผ๐–ผโข(a). Thus, we can define f(a):โ‰ก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 nonempty if it is unequal to the empty subset (ฮปx.โŠฅ):๐’ซ(X). We leave it to the reader to verify that assuming excluded middle, this is equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmath to mere inhabitation, i.e.ย to the condition โˆƒ(x:A).xโˆˆB.

Lemma 10.3.8.

Assuming excluded middle, < is well-founded if and only if every nonempty subset B:Pโข(A) merely has a minimal element.


Suppose first < is well-founded, and suppose BโŠ†A is a subset with no minimal element. That is, for any a:A with aโˆˆB, there merely exists a b:A with b<a and bโˆˆB.

We claim that for any a:A and s:๐–บ๐–ผ๐–ผโข(a), we have aโˆ‰B. By induction, we may assume s is a function assigning to each aโ€ฒ<a a proof sโข(aโ€ฒ):๐–บ๐–ผ๐–ผโข(a), and that moreover for each such aโ€ฒ we have aโ€ฒโˆ‰B. If aโˆˆB, then by assumptionPlanetmathPlanetmath, there would merely exist a b<a with bโˆˆB, which contradicts this assumption. Thus, aโˆ‰B; this completesPlanetmathPlanetmathPlanetmath the induction. Since < is well-founded, we have aโˆ‰B for all a:A, i.e. B is empty.

Now suppose each nonempty subset merely has a minimal element. Let B=\setofa:A|ยฌ๐–บ๐–ผ๐–ผ(a). Then if B is nonempty, it merely has a minimal element. Thus there merely exists an a:A with aโˆˆB such that for all b<a, we have ๐–บ๐–ผ๐–ผโข(b). But then by definition (and induction on truncation), a is merely accessible, and hence accessible, contradicting aโˆˆB. Thus, B is empty, so < is well-founded. โˆŽ

Definition 10.3.9.

A well-founded relation < on a set A is extensional if for any a,b: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 theoryMathworldPlanetmath.

Theorem 10.3.10.

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


By the univalence axiom, it suffices to show that if (A,<) is extensional and well-founded and f:(A,<)โ‰…(A,<), then f=๐—‚๐–ฝA. We prove by induction on < that fโข(a)=a for all a:A. The inductive hypothesis is that for all aโ€ฒ<a, we have fโข(aโ€ฒ)=aโ€ฒ.

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


However, since f is an automorphismMathworldPlanetmathPlanetmathPlanetmathPlanetmath, we have (c<a)โ‡”(f(c)<f(a)). But c<a implies fโข(c)=c by the inductive hypothesis, so (c<a)โ†’(c<f(a)). On the other hand, if c<fโข(a), then f-1โข(c)<a, and so c=fโข(f-1โข(c))=f-1โข(c) by the inductive hypothesis again; thus c<a. Therefore, we have (c<a)โ‡”(c<f(a)) for any c:A, so fโข(a)=a. โˆŽ

Definition 10.3.11.

If (A,<) and (B,<) are extensional and well-founded, a simulation is a function f:Aโ†’B such that

  1. 1.

    if a<aโ€ฒ, then fโข(a)<fโข(aโ€ฒ), and

  2. 2.

    for all a:A and b:B, if b<fโข(a), then there merely exists an aโ€ฒ<a with fโข(aโ€ฒ)=b.

Lemma 10.3.12.

Any simulation is injectivePlanetmathPlanetmath.


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 aโ€ฒ<a, and any b:B, if fโข(aโ€ฒ)=fโข(b) then a=b. The inner inductive hypothesis for b:A says that for any bโ€ฒ<b, if fโข(a)=fโข(bโ€ฒ) then a=bโ€ฒ.

Suppose fโข(a)=fโข(b); we must show a=b. By extensionality, it suffices to show that for any c:A we have (c<a)โ‡”(c<b). If c<a, then fโข(c)<fโข(a) by \autorefdef:simulation1. Hence fโข(c)<fโข(b), so by \autorefdef:simulation2 there merely exists cโ€ฒ:A with cโ€ฒ<b and fโข(c)=fโข(cโ€ฒ). By the inductive hypothesis for a, we have c=cโ€ฒ, hence c<b. The dual argument is symmetrical. โˆŽ

In particular, this implies that in \autorefdef:simulation2 the word โ€œmerelyโ€ could be omitted without change of sense.

Corollary 10.3.13.

If f:Aโ†’B is a simulation, then for all a:A and b:B, if b<fโข(a), there purely exists an aโ€ฒ<a with fโข(aโ€ฒ)=b.


Since f is injective, โˆ‘(a:A)(f(a)=b) is a mere proposition. โˆŽ

We say that a subset C:๐’ซโข(B) is an initial segment if cโˆˆC and b<c imply bโˆˆ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โ†’B is equal to the inclusion of some initial segment of B.

Theorem 10.3.14.

For a set A, let Pโข(A) be the type of extensional well-founded relations on A. If <A:Pโข(A) and <B:Pโข(B) and f:Aโ†’B, let H<Aโข<Bโข(f) be the mere proposition that f is a simulation. Then (P,H) is a standard notion of structureMathworldPlanetmath over Sโขeโขt in the sense of \autorefsec:sip.


We leave it to the reader to verify that identitiesPlanetmathPlanetmathPlanetmathPlanetmath are simulations, and that composites of simulations are simulations. Thus, we have a notion of structure. For standardness, we must show that if < and โ‰บ are two extensional well-founded relations on A, and ๐—‚๐–ฝA is a simulation in both directions, then < and โ‰บ are equal. Since extensionality and well-foundedness are mere propositions, for this it suffices to have โˆ€(a,b:A).(a<b)โ‡”(aโ‰บb). But this follows from \autorefdef:simulation1 for ๐—‚๐–ฝ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 (A,<) and (B,<), there is at most one simulation f:Aโ†’B.


Suppose f,g:Aโ†’B are simulations. Since being a simulation is a mere property, it suffices to show โˆ€(a:A).(f(a)=g(a)). By induction on <, we may suppose fโข(aโ€ฒ)=gโข(aโ€ฒ) for all aโ€ฒ<a. And by extensionality of B, to have fโข(a)=gโข(a) it suffices to have โˆ€(b:B).(b<f(a))โ‡”(b<g(a)).

But since f is a simulation, if b<fโข(a), then we have aโ€ฒ<a with fโข(aโ€ฒ)=b. By the inductive hypothesis, we have also gโข(aโ€ฒ)=b, hence b<gโข(a). The dual argument is symmetrical. โˆŽ

Thus, if A and B are equipped with extensional and well-founded relations, we may write Aโ‰คB to mean there exists a simulation f:Aโ†’B. \autorefthm:wfcat implies that if Aโ‰คB and Bโ‰คA, then A=B.

Definition 10.3.17.

An ordinalMathworldPlanetmathPlanetmath is a set A with an extensional well-founded relation which is transitiveMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath, i.e.ย satisfies โˆ€(a,b,c:A).(a<b)โ†’(b<c)โ†’(a<c).

Example 10.3.18.

Of course, the usual strict order on N is transitive. It is easily seen to be extensional as well; thus it is an ordinal. As usual, we denote this ordinal by ฯ‰.

Let ๐–ฎ๐—‹๐–ฝ denote the type of ordinals. By the previous results, ๐–ฎ๐—‹๐–ฝ is a set and has a natural partial orderMathworldPlanetmath. We now show that ๐–ฎ๐—‹๐–ฝ also admits a well-founded relation.

If A is an ordinal and a:A, let A/a:โ‰ก\setofb:A|b<a denote the initial segment. Note that if A/a=A/b as ordinals, then that isomorphismPlanetmathPlanetmath 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โ†ฆA/a is an injection Aโ†’๐–ฎ๐—‹๐–ฝ.

Definition 10.3.19.

For ordinals A and B, a simulation f:Aโ†’B is said to be bounded if there exists b:B such that A=B/b.

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

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

Theorem 10.3.20.

(๐–ฎ๐—‹๐–ฝ,<) is an ordinal.

More precisely, this theorem says that the type ๐–ฎ๐—‹๐–ฝ๐’ฐi of ordinals in one universePlanetmathPlanetmath is itself an ordinal in the next higher universe, i.e.ย (๐–ฎ๐—‹๐–ฝ๐’ฐi,<):๐–ฎ๐—‹๐–ฝ๐’ฐi+1.


Let A be an ordinal; we first show that A/a is accessible (in ๐–ฎ๐—‹๐–ฝ) for all a:A. By well-founded induction on A, suppose A/b is accessible for all b<a. By definition of accessibility, we must show that B is accessible in ๐–ฎ๐—‹๐–ฝ for all B<A/a. However, if B<A/a then there is some b<a 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 ๐–ฎ๐—‹๐–ฝ, by definition we must show B is accessible for all B<A. But as before, B<A means B=A/a for some a:A, which is accessible as we just proved. Thus, ๐–ฎ๐—‹๐–ฝ is well-founded.

For extensionality, suppose A and B are ordinals such that โˆ(C:๐–ฎ๐—‹๐–ฝ)(C<A)โ‡”(C<B). Then for every a:A, since A/a<A, we have A/a<B, hence there is b:B with A/a=B/b. Define f:Aโ†’B to take each a to the corresponding b; it is straightforward to verify that f is an isomorphism. Thus Aโ‰…B, hence A=B by univalence.

Finally, it is easy to see that < is transitive. โˆŽ

Treating ๐–ฎ๐—‹๐–ฝ 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 U be a universe. For any A:OrdU, there is a B:OrdU such that A<B.


Let B=A+๐Ÿ, with the element โ‹†:๐Ÿ being greater than all elements of A. Then B is an ordinal and it is easy to see that Aโ‰…B/โ‹†. โˆŽ

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 \autorefthm:ordsucc.

Note that C<A if and only if C=A/a for some a:A. This gives an isomorphism Aโ‰…๐–ฎ๐—‹๐–ฝ/A, so that A<๐–ฎ๐—‹๐–ฝ. Thus we may take B:โ‰ก๐–ฎ๐—‹๐–ฝ. โˆŽ

The second proof would be valid if we had stated \autorefthm:ordsucc in a typically ambiguous style. But the resulting lemma would be less useful, because the second proof would constrain the second โ€œ๐–ฎ๐—‹๐–ฝโ€ 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.

SimilarMathworldPlanetmath remarks apply to the next lemma, which could be proved in a less useful way by observing that Aโ‰ค๐–ฎ๐—‹๐–ฝ for any A:๐–ฎ๐—‹๐–ฝ.

Lemma 10.3.22.

Let U be a universe. For any X:U and F:Xโ†’OrdU, there exists B:OrdU such that Fโขxโ‰คB for all x:X.


Let B be the quotient of the equivalence relation โˆผ on โˆ‘(x:X)Fโขx defined as follows:


Define (x,y)<(xโ€ฒ,yโ€ฒ) if (Fโขx)/y<(Fโขxโ€ฒ)/yโ€ฒ. This clearly descends to the quotient, and can be seen to make B into an ordinal. Moreover, for each x:X the induced map Fโขxโ†’B is a simulation. โˆŽ

Title 10.3 Ordinal numbers