# 10.3 Ordinal numbers

###### Definition 10.3.1.

Let $A$ be a set and

 $(\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}<\mathord{\hskip 1.0pt\text{--}% \hskip 1.0pt}):A\to A\to\mathsf{Prop}$

a binary relation on $A$. We define by induction what it means for an element $a:A$ to be by $<$:

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

We write $\mathsf{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, 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:generalizations. More precisely, it has one constructor, say $\mathsf{acc}_{<}$, with type

 $\mathsf{acc}_{<}:\mathchoice{\prod_{a:A}\,}{\mathchoice{{\textstyle\prod_{(a:A% )}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle% \prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{% \textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}\Bigl{(% }\mathchoice{\prod_{b:A}\,}{\mathchoice{{\textstyle\prod_{(b:A)}}}{\prod_{(b:A% )}}{\prod_{(b:A)}}{\prod_{(b:A)}}}{\mathchoice{{\textstyle\prod_{(b:A)}}}{% \prod_{(b:A)}}{\prod_{(b:A)}}{\prod_{(b:A)}}}{\mathchoice{{\textstyle\prod_{(b% :A)}}}{\prod_{(b:A)}}{\prod_{(b:A)}}{\prod_{(b:A)}}}(b

The induction principle for $\mathsf{acc}$ says that for any $P:\mathchoice{\prod_{a:A}\,}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:% A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{% \prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a% :A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}\mathsf{acc}(a)\to\mathcal% {U}$, if we have

 $f:\mathchoice{\prod_{(a:A)}\,}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(% a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{% \prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a% :A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}\mathchoice{\prod_{(h:% \mathchoice{\prod_{b:A}\,}{\mathchoice{{\textstyle\prod_{(b:A)}}}{\prod_{(b:A)% }}{\prod_{(b:A)}}{\prod_{(b:A)}}}{\mathchoice{{\textstyle\prod_{(b:A)}}}{\prod% _{(b:A)}}{\prod_{(b:A)}}{\prod_{(b:A)}}}{\mathchoice{{\textstyle\prod_{(b:A)}}% }{\prod_{(b:A)}}{\prod_{(b:A)}}{\prod_{(b:A)}}}(b

then we have $g:\mathchoice{\prod_{(a:A)}\,}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(% a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{% \prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a% :A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}\mathchoice{\prod_{(c:% \mathsf{acc}(a))}\,}{\mathchoice{{\textstyle\prod_{(c:\mathsf{acc}(a))}}}{% \prod_{(c:\mathsf{acc}(a))}}{\prod_{(c:\mathsf{acc}(a))}}{\prod_{(c:\mathsf{% acc}(a))}}}{\mathchoice{{\textstyle\prod_{(c:\mathsf{acc}(a))}}}{\prod_{(c:% \mathsf{acc}(a))}}{\prod_{(c:\mathsf{acc}(a))}}{\prod_{(c:\mathsf{acc}(a))}}}{% \mathchoice{{\textstyle\prod_{(c:\mathsf{acc}(a))}}}{\prod_{(c:\mathsf{acc}(a)% )}}{\prod_{(c:\mathsf{acc}(a))}}{\prod_{(c:\mathsf{acc}(a))}}}P(a,c)$ defined by induction, with

 $g(a,\mathsf{acc}_{<}(a,h))\equiv f(a,\,h,\,{\lambda}b.\,{\lambda}l.\,g(b,h(b,l% ))).$

This is a mouthful, but generally we apply it only in the simpler case where $P:A\to\mathcal{U}$ 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

 $f:\mathchoice{\prod_{a:A}\,}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:% A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{% \prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a% :A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}\Bigl{(}\mathchoice{\prod_% {b:A}\,}{\mathchoice{{\textstyle\prod_{(b:A)}}}{\prod_{(b:A)}}{\prod_{(b:A)}}{% \prod_{(b:A)}}}{\mathchoice{{\textstyle\prod_{(b:A)}}}{\prod_{(b:A)}}{\prod_{(% b:A)}}{\prod_{(b:A)}}}{\mathchoice{{\textstyle\prod_{(b:A)}}}{\prod_{(b:A)}}{% \prod_{(b:A)}}{\prod_{(b:A)}}}(b

That is, we assume every $b 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}:\mathsf{acc}(a)$ we have $s_{1}=s_{2}$. We prove this by induction on $s_{1}$, with

 $P_{1}(a,s_{1}):\!\!\equiv\mathchoice{\prod_{s_{2}:\mathsf{acc}(a)}\,}{% \mathchoice{{\textstyle\prod_{(s_{2}:\mathsf{acc}(a))}}}{\prod_{(s_{2}:\mathsf% {acc}(a))}}{\prod_{(s_{2}:\mathsf{acc}(a))}}{\prod_{(s_{2}:\mathsf{acc}(a))}}}% {\mathchoice{{\textstyle\prod_{(s_{2}:\mathsf{acc}(a))}}}{\prod_{(s_{2}:% \mathsf{acc}(a))}}{\prod_{(s_{2}:\mathsf{acc}(a))}}{\prod_{(s_{2}:\mathsf{acc}% (a))}}}{\mathchoice{{\textstyle\prod_{(s_{2}:\mathsf{acc}(a))}}}{\prod_{(s_{2}% :\mathsf{acc}(a))}}{\prod_{(s_{2}:\mathsf{acc}(a))}}{\prod_{(s_{2}:\mathsf{acc% }(a))}}}(s_{1}=s_{2}).$

Thus, we must show that for any $a:A$ and ${h_{1}:\mathchoice{\prod_{b:A}\,}{\mathchoice{{\textstyle\prod_{(b:A)}}}{\prod% _{(b:A)}}{\prod_{(b:A)}}{\prod_{(b:A)}}}{\mathchoice{{\textstyle\prod_{(b:A)}}% }{\prod_{(b:A)}}{\prod_{(b:A)}}{\prod_{(b:A)}}}{\mathchoice{{\textstyle\prod_{% (b:A)}}}{\prod_{(b:A)}}{\prod_{(b:A)}}{\prod_{(b:A)}}}(b and

 $k_{1}:{\mathchoice{\prod_{(b:A)}\,}{\mathchoice{{\textstyle\prod_{(b:A)}}}{% \prod_{(b:A)}}{\prod_{(b:A)}}{\prod_{(b:A)}}}{\mathchoice{{\textstyle\prod_{(b% :A)}}}{\prod_{(b:A)}}{\prod_{(b:A)}}{\prod_{(b:A)}}}{\mathchoice{{\textstyle% \prod_{(b:A)}}}{\prod_{(b:A)}}{\prod_{(b:A)}}{\prod_{(b:A)}}}\mathchoice{\prod% _{(l:b

we have $\mathsf{acc}_{<}(a,h)=s_{2}$ for any $s_{2}:\mathsf{acc}(a)$. We regard this statement as $\mathchoice{\prod_{(a:A)}\,}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:% A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{% \prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a% :A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}\mathchoice{\prod_{(s_{2}:% \mathsf{acc}(a))}\,}{\mathchoice{{\textstyle\prod_{(s_{2}:\mathsf{acc}(a))}}}{% \prod_{(s_{2}:\mathsf{acc}(a))}}{\prod_{(s_{2}:\mathsf{acc}(a))}}{\prod_{(s_{2% }:\mathsf{acc}(a))}}}{\mathchoice{{\textstyle\prod_{(s_{2}:\mathsf{acc}(a))}}}% {\prod_{(s_{2}:\mathsf{acc}(a))}}{\prod_{(s_{2}:\mathsf{acc}(a))}}{\prod_{(s_{% 2}:\mathsf{acc}(a))}}}{\mathchoice{{\textstyle\prod_{(s_{2}:\mathsf{acc}(a))}}% }{\prod_{(s_{2}:\mathsf{acc}(a))}}{\prod_{(s_{2}:\mathsf{acc}(a))}}{\prod_{(s_% {2}:\mathsf{acc}(a))}}}P_{2}(a,s_{2})$, where

 $P_{2}(a,s_{2}):\!\!\equiv\mathchoice{\prod_{(h_{1}:\cdots)}\,}{\mathchoice{{% \textstyle\prod_{(h_{1}:\cdots)}}}{\prod_{(h_{1}:\cdots)}}{\prod_{(h_{1}:% \cdots)}}{\prod_{(h_{1}:\cdots)}}}{\mathchoice{{\textstyle\prod_{(h_{1}:\cdots% )}}}{\prod_{(h_{1}:\cdots)}}{\prod_{(h_{1}:\cdots)}}{\prod_{(h_{1}:\cdots)}}}{% \mathchoice{{\textstyle\prod_{(h_{1}:\cdots)}}}{\prod_{(h_{1}:\cdots)}}{\prod_% {(h_{1}:\cdots)}}{\prod_{(h_{1}:\cdots)}}}\mathchoice{\prod_{(k_{1}:\cdots)}\,% }{\mathchoice{{\textstyle\prod_{(k_{1}:\cdots)}}}{\prod_{(k_{1}:\cdots)}}{% \prod_{(k_{1}:\cdots)}}{\prod_{(k_{1}:\cdots)}}}{\mathchoice{{\textstyle\prod_% {(k_{1}:\cdots)}}}{\prod_{(k_{1}:\cdots)}}{\prod_{(k_{1}:\cdots)}}{\prod_{(k_{% 1}:\cdots)}}}{\mathchoice{{\textstyle\prod_{(k_{1}:\cdots)}}}{\prod_{(k_{1}:% \cdots)}}{\prod_{(k_{1}:\cdots)}}{\prod_{(k_{1}:\cdots)}}}(\mathsf{acc}_{<}(a,% h_{1})=s_{2});$

thus we may prove it by induction on $s_{2}$. Therefore, we assume $h_{2}:\mathchoice{\prod_{b:A}\,}{\mathchoice{{\textstyle\prod_{(b:A)}}}{\prod_% {(b:A)}}{\prod_{(b:A)}}{\prod_{(b:A)}}}{\mathchoice{{\textstyle\prod_{(b:A)}}}% {\prod_{(b:A)}}{\prod_{(b:A)}}{\prod_{(b:A)}}}{\mathchoice{{\textstyle\prod_{(% b:A)}}}{\prod_{(b:A)}}{\prod_{(b:A)}}{\prod_{(b:A)}}}(b, 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 $\mathsf{acc}_{<}(a,h_{1})=\mathsf{acc}_{<}(a,h_{2})$. By function extensionality, it suffices to show $h_{1}(b,l)=h_{2}(b,l)$ for all $b:A$ and $l:b. This follows from $k_{1}$. ∎

###### 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\to\mathcal{U}$, we can use the induction principle of $\mathsf{acc}$ to conclude $\mathchoice{\prod_{a:A}\,}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)% }}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod% _{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}% }{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}\mathsf{acc}(a)\to P(a)$, and then apply well-foundedness to conclude $\mathchoice{\prod_{a:A}\,}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)% }}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod% _{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}% }{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}P(a)$. In other words, if from $\forall(b:A).\,(b 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 $\mathchoice{\prod_{a:A}\,}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)% }}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod% _{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}% }{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}\mathsf{acc}(a)$, which is a mere proposition since each $\mathsf{acc}(a)$ is. ∎

###### Example 10.3.5.

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

Specifically, we prove by induction on $n:\mathbb{N}$ that $k$ is accessible for all $k\leq 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\leq n$, which is to say for all $k; hence by definition $n+1$ is also accessible.

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

###### Example 10.3.6.

Let $A:\set$ and $B:A\to\set$ be a family of sets. Recall from \autorefsec:w-types that the $W$-type $\mathchoice{\mathchoice{{\textstyle\mathsf{W}_{(a:A)}}}{\mathsf{W}_{(a:A)}}{% \mathsf{W}_{(a:A)}}{\mathsf{W}_{(a:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(a% :A)}}}{\mathsf{W}_{(a:A)}}{\mathsf{W}_{(a:A)}}{\mathsf{W}_{(a:A)}}}{% \mathchoice{{\textstyle\mathsf{W}_{(a:A)}}}{\mathsf{W}_{(a:A)}}{\mathsf{W}_{(a% :A)}}{\mathsf{W}_{(a:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(a:A)}}}{\mathsf% {W}_{(a:A)}}{\mathsf{W}_{(a:A)}}{\mathsf{W}_{(a:A)}}}B(a)$ is inductively generated by the single constructor

• ${\mathsf{sup}}:\mathchoice{\prod_{a:A}\,}{\mathchoice{{\textstyle\prod_{(a:A)}% }}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_% {(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{% \textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}(B(a)% \to\mathchoice{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}% {\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(% x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{% \mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x% :A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf% {W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}B(x))\to\mathchoice{% \mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x% :A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf% {W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle% \mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)% }}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}% _{(x:A)}}{\mathsf{W}_{(x:A)}}}B(x)$

We define the relation $<$ on $\mathchoice{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{% \mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x% :A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{% \mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x% :A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf% {W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}B(x)$ by recursion on its second argument:

• For any $a:A$ and $f:B(a)\to\mathchoice{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(% x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf% {W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{% \mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x% :A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf% {W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}B(x)$, we define $w<{\mathsf{sup}}(a,f)$ to mean that there merely exists a $b:B(a)$ such that $w=f(b)$.

Now we prove that every $w:\mathchoice{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{% \mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x% :A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{% \mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x% :A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf% {W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}B(x)$ is accessible for this relation, using the usual induction principle for $\mathchoice{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{% \mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x% :A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{% \mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x% :A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf% {W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}B(x)$. This means we assume given $a:A$ and $f:B(a)\to\mathchoice{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(% x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf% {W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{% \mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x% :A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf% {W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}B(x)$, and also a lifting $f^{\prime}:\mathchoice{\prod_{b:B(a)}\,}{\mathchoice{{\textstyle\prod_{(b:B(a)% )}}}{\prod_{(b:B(a))}}{\prod_{(b:B(a))}}{\prod_{(b:B(a))}}}{\mathchoice{{% \textstyle\prod_{(b:B(a))}}}{\prod_{(b:B(a))}}{\prod_{(b:B(a))}}{\prod_{(b:B(a% ))}}}{\mathchoice{{\textstyle\prod_{(b:B(a))}}}{\prod_{(b:B(a))}}{\prod_{(b:B(% a))}}{\prod_{(b:B(a))}}}\mathsf{acc}(f(b))$. But then by definition of $<$, we have $\mathsf{acc}(w)$ for all $w<{\mathsf{sup}}(a,f)$; hence ${\mathsf{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 $\mathcal{P}(B)$ denotes the power set $\mathcal{P}(B):\!\!\equiv(B\to\mathsf{Prop})$.

###### Lemma 10.3.7.

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

 $g:\mathcal{P}(B)\to B$

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

 $f(a)=g\Big{(}\setof{f(a^{\prime})|a^{\prime}

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

###### Proof.

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

 $\bar{f}(a,s):\!\!\equiv g\Big{(}\setof{\bar{f}(a^{\prime},s(a^{\prime}))|a^{% \prime}

Now since $<$ is well-founded, we have a function $w:\mathchoice{\prod_{a:A}\,}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:% A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{% \prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a% :A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}\mathsf{acc}(a)$. Thus, we can define $f(a):\!\!\equiv\bar{f}(a,w(a))$. ∎

In classical logic, well-foundedness has a more well-known reformulation. In the following, we say that a subset $B:\mathcal{P}(A)$ is nonempty if it is unequal to the empty subset $({\lambda}x.\,\bot):\mathcal{P}(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:\mathcal{P}(A)$ 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 $b and $b\in B$.

We claim that for any $a:A$ and $s:\mathsf{acc}(a)$, we have $a\notin B$. By induction, we may assume $s$ is a function assigning to each $a^{\prime} a proof $s(a^{\prime}):\mathsf{acc}(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 $b 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=\setof{a:A|\neg\mathsf{acc}(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 $b, we have $\mathsf{acc}(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 extensional if for any $a,b:A$, we have

 $\Bigl{(}\forall(c:A).\,(c

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 $(A,<)$ is extensional and well-founded and $f:(A,<)\cong(A,<)$, then $f=\mathsf{id}_{A}$. We prove by induction on $<$ that $f(a)=a$ for all $a:A$. The inductive hypothesis is that for all $a^{\prime}, we have $f(a^{\prime})=a^{\prime}$.

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

 $\forall(c:A).\,(c

However, since $f$ is an automorphism, we have $(c. But $c implies $f(c)=c$ by the inductive hypothesis, so $(c. On the other hand, if $c, then $f^{-1}(c), and so $c=f(f^{-1}(c))=f^{-1}(c)$ by the inductive hypothesis again; thus $c. Therefore, we have $(c 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\to B$ such that

1. 1.

if $a, then $f(a), and

2. 2.

for all $a:A$ and $b:B$, if $b, then there merely exists an $a^{\prime} 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 $a^{\prime}, and any $b:B$, if $f(a^{\prime})=f(b)$ then $a=b$. The inner inductive hypothesis for $b:A$ says that for any $b^{\prime}, 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 $(c. If $c, then $f(c) by \autorefdef:simulation1. Hence $f(c), so by \autorefdef:simulation2 there merely exists $c^{\prime}:A$ with $c^{\prime} and $f(c)=f(c^{\prime})$. By the inductive hypothesis for $a$, we have $c=c^{\prime}$, hence $c. 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\to B$ is a simulation, then for all $a:A$ and $b:B$, if $b, there purely exists an $a^{\prime} with $f(a^{\prime})=b$.

###### Proof.

Since $f$ is injective, $\mathchoice{\sum_{a:A}\,}{\mathchoice{{\textstyle\sum_{(a:A)}}}{\sum_{(a:A)}}{% \sum_{(a:A)}}{\sum_{(a:A)}}}{\mathchoice{{\textstyle\sum_{(a:A)}}}{\sum_{(a:A)% }}{\sum_{(a:A)}}{\sum_{(a:A)}}}{\mathchoice{{\textstyle\sum_{(a:A)}}}{\sum_{(a% :A)}}{\sum_{(a:A)}}{\sum_{(a:A)}}}(f(a)=b)$ is a mere proposition. ∎

We say that a subset $C:\mathcal{P}(B)$ is an initial segment if $c\in C$ and $b 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(A)$ be the type of extensional well-founded relations on $A$. If $\mathord{<_{A}}:P(A)$ and $\mathord{<_{B}}:P(B)$ and $f:A\to B$, let $H_{\mathord{<_{A}}\mathord{<_{B}}}(f)$ be the mere proposition that $f$ is a simulation. Then $(P,H)$ is a standard notion of structure over $\mathcal{S}et$ in the sense of \autorefsec: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 $\mathsf{id}_{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 $\forall(a,b:A).\,(a. But this follows from \autorefdef:simulation1 for $\mathsf{id}_{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\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 $a^{\prime}. And by extensionality of $B$, to have $f(a)=g(a)$ it suffices to have $\forall(b:B).\,(b.

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

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

###### Definition 10.3.17.

An is a set $A$ with an extensional well-founded relation which is transitive, i.e. satisfies $\forall(a,b,c:A).\,(a.

###### Example 10.3.18.

Of course, the usual strict order on $\mathbb{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 $\mathsf{Ord}$ denote the type of ordinals. By the previous results, $\mathsf{Ord}$ is a set and has a natural partial order. We now show that $\mathsf{Ord}$ also admits a well-founded relation.

If $A$ is an ordinal and $a:A$, let ${A}_{/a}:\!\!\equiv\setof{b:A|b 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\mathsf{Ord}$.

###### Definition 10.3.19.

For ordinals $A$ and $B$, a simulation $f:A\to 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 if there exists a bounded simulation from $A$ to $B$. Since simulations are unique, $A is also a mere proposition.

###### Theorem 10.3.20.

$(\mathsf{Ord},<)$ is an ordinal.

More precisely, this theorem says that the type $\mathsf{Ord}_{\mathcal{U}_{i}}$ of ordinals in one universe is itself an ordinal in the next higher universe, i.e. $(\mathsf{Ord}_{\mathcal{U}_{i}},<):\mathsf{Ord}_{\mathcal{U}_{i+1}}$.

###### Proof.

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

For extensionality, suppose $A$ and $B$ are ordinals such that $\mathchoice{\prod_{C:\mathsf{Ord}}\,}{\mathchoice{{\textstyle\prod_{(C:\mathsf% {Ord})}}}{\prod_{(C:\mathsf{Ord})}}{\prod_{(C:\mathsf{Ord})}}{\prod_{(C:% \mathsf{Ord})}}}{\mathchoice{{\textstyle\prod_{(C:\mathsf{Ord})}}}{\prod_{(C:% \mathsf{Ord})}}{\prod_{(C:\mathsf{Ord})}}{\prod_{(C:\mathsf{Ord})}}}{% \mathchoice{{\textstyle\prod_{(C:\mathsf{Ord})}}}{\prod_{(C:\mathsf{Ord})}}{% \prod_{(C:\mathsf{Ord})}}{\prod_{(C:\mathsf{Ord})}}}(C Then for every $a:A$, since ${A}_{/a}, we have ${A}_{/a}, 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 $\mathsf{Ord}$ 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 $\mathcal{U}$ be a universe. For any $A:\mathsf{Ord}_{\mathcal{U}}$, there is a $B:\mathsf{Ord}_{\mathcal{U}}$ such that $A.

###### Proof.

Let $B=A+\mathbf{1}$, with the element $\star:\mathbf{1}$ 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 $\mathcal{U}$ to denote an arbitrary, unspecified universe. Consider the following alternative proof of it.

###### Another putative proof of \autorefthm:ordsucc.

Note that $C if and only if $C={A}_{/a}$ for some $a:A$. This gives an isomorphism $A\cong{\mathsf{Ord}}_{/A}$, so that $A<\mathsf{Ord}$. Thus we may take $B:\!\!\equiv\mathsf{Ord}$. ∎

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 “$\mathsf{Ord}$” 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\leq\mathsf{Ord}$ for any $A:\mathsf{Ord}$.

###### Lemma 10.3.22.

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

###### Proof.

Let $B$ be the quotient of the equivalence relation $\sim$ on $\mathchoice{\sum_{x:X}\,}{\mathchoice{{\textstyle\sum_{(x:X)}}}{\sum_{(x:X)}}{% \sum_{(x:X)}}{\sum_{(x:X)}}}{\mathchoice{{\textstyle\sum_{(x:X)}}}{\sum_{(x:X)% }}{\sum_{(x:X)}}{\sum_{(x:X)}}}{\mathchoice{{\textstyle\sum_{(x:X)}}}{\sum_{(x% :X)}}{\sum_{(x:X)}}{\sum_{(x:X)}}}Fx$ defined as follows:

 $(x,y)\sim(x^{\prime},y^{\prime})\;:\!\!\equiv\;\Big{(}{(Fx)}_{/y}\cong{(Fx^{% \prime})}_{/y^{\prime}}\Big{)}.$

Define $(x,y)<(x^{\prime},y^{\prime})$ if ${(Fx)}_{/y}<{(Fx^{\prime})}_{/y^{\prime}}$. 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. ∎

Title 10.3 Ordinal numbers
\metatable