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 accessible by $<$ :

•

If $b$ is accessible for every $b<a$ , 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<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: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<a)\to\mathsf{acc}(b)% \Bigr{)}\to\mathsf{acc}(a).

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<a)\to\mathsf{acc}(b))}\,}{% \mathchoice{{\textstyle\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<a)\to\mathsf{acc}(b))}}}{\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<a)\to\mathsf{acc}(b))}}{\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<a)\to\mathsf{acc}(b))}}{\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<a)\to\mathsf{acc}(b))}}}{\mathchoice{{% \textstyle\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<a)% \to\mathsf{acc}(b))}}}{\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<a)\to\mathsf{acc}(b))}}{\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<a)\to\mathsf{acc}(b))}}{\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<a)\to\mathsf{acc}(b))}}}{\mathchoice{{% \textstyle\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<a)% \to\mathsf{acc}(b))}}}{\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<a)\to\mathsf{acc}(b))}}{\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<a)\to\mathsf{acc}(b))}}{\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<a)\to\mathsf{acc}(b))}}}\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)}}}\mathchoice{\prod_{(l:b<a)}\,}{% \mathchoice{{\textstyle\prod_{(l:b<a)}}}{\prod_{(l:b<a)}}{\prod_{(l:b<a)}}{% \prod_{(l:b<a)}}}{\mathchoice{{\textstyle\prod_{(l:b<a)}}}{\prod_{(l:b<a)}}{% \prod_{(l:b<a)}}{\prod_{(l:b<a)}}}{\mathchoice{{\textstyle\prod_{(l:b<a)}}}{% \prod_{(l:b<a)}}{\prod_{(l:b<a)}}{\prod_{(l:b<a)}}}P(b,h(b,l))\Bigr{)}\to P(a,% \mathsf{acc}_{<}(a,h)),

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<a)\to\mathsf{acc}(b)\times P(b)\Bigr{)}\to P(% a).

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.

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<a)\to\mathsf{acc}(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<a)}\,}{\mathchoice{{\textstyle\prod_{(l:b<a)}}}{\prod_{(l:b<a)}}{\prod_% {(l:b<a)}}{\prod_{(l:b<a)}}}{\mathchoice{{\textstyle\prod_{(l:b<a)}}}{\prod_{(% l:b<a)}}{\prod_{(l:b<a)}}{\prod_{(l:b<a)}}}{\mathchoice{{\textstyle\prod_{(l:b% <a)}}}{\prod_{(l:b<a)}}{\prod_{(l:b<a)}}{\prod_{(l:b<a)}}}\mathchoice{\prod_{(% t:\mathsf{acc}(b))}\,}{\mathchoice{{\textstyle\prod_{(t:\mathsf{acc}(b))}}}{% \prod_{(t:\mathsf{acc}(b))}}{\prod_{(t:\mathsf{acc}(b))}}{\prod_{(t:\mathsf{% acc}(b))}}}{\mathchoice{{\textstyle\prod_{(t:\mathsf{acc}(b))}}}{\prod_{(t:% \mathsf{acc}(b))}}{\prod_{(t:\mathsf{acc}(b))}}{\prod_{(t:\mathsf{acc}(b))}}}{% \mathchoice{{\textstyle\prod_{(t:\mathsf{acc}(b))}}}{\prod_{(t:\mathsf{acc}(b)% )}}{\prod_{(t:\mathsf{acc}(b))}}{\prod_{(t:\mathsf{acc}(b))}}}h_{1}(b,l)=t},

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<a)\to\mathsf{acc}(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<a$ . 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<a)\to P(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<n+1$ ; 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}<a}\Big{)}.

(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$ 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}<a}\Big{)}.

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<a$ 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$ 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<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=\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<a$ , 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<a)\Leftrightarrow(c<b)\Bigr{)}\to(a=b).

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}<a$ , 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<f(a))\Leftrightarrow(c<a).

However, since $f$ is an automorphism, we have $(c<a)\Leftrightarrow(f(c)<f(a))$ . But $c<a$ implies $f(c)=c$ by the inductive hypothesis, so $(c<a)\to(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)\Leftrightarrow(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\to B$ such that

1.

if $a<a^{\prime}$ , then $f(a)<f(a^{\prime})$ , and
2.

for all $a : A$ and $b : B$ , if $b<f(a)$ , then there merely exists an $a^{\prime}<a$ 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}<a$ , 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}<b$ , 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<a)\Leftrightarrow(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^{\prime}:A$ with $c^{\prime}<b$ and $f(c)=f(c^{\prime})$ . By the inductive hypothesis for $a$ , we have $c=c^{\prime}$ , 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\to B$ is a simulation, then for all $a : A$ and $b : B$ , if $b<f(a)$ , there purely exists an $a^{\prime}<a$ 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<c$ 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<b)\Leftrightarrow(a\prec b)$ . 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}<a$ . And by extensionality of $B$ , to have $f(a)=g(a)$ it suffices to have $\forall(b:B).\,(b<f(a))\Leftrightarrow(b<g(a))$ .

But since $f$ is a simulation, if $b<f(a)$ , then we have $a^{\prime}<a$ with $f(a^{\prime})=b$ . By the inductive hypothesis, we have also $g(a^{\prime})=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\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 ordinal is a set $A$ with an extensional well-founded relation which is transitive, i.e. satisfies $\forall(a,b,c:A).\,(a<b)\to(b<c)\to(a<c)$ .

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<a}$ 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<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.

$(\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<a$ . 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<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 $\mathsf{Ord}$ , 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, $\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<A)\Leftrightarrow(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\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<B$ .

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<A$ 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