10.3 Ordinal numbers
It may seem that such an inductive definition can never get off the ground, but of course if has the property that there are no such that , then 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 , with type
The induction principle for says that for any , if we have
then we have defined by induction, with
This is a mouthful, but generally we apply it only in the simpler case where depends only on . In this case the second and third arguments of may be combined, so that what we have to prove is
That is, we assume every is accessible and is defined, and from these define .
The omission of the second argument of is justified by the following lemma, whose proof is the only place where we use the more general form of the induction principle.
Accessibility is a mere property.
We must show that for any and we have . We prove this by induction on , with
Thus, we must show that for any and and
we have for any . We regard this statement as , where
thus we may prove it by induction on . Therefore, we assume , and with a monstrous but irrelevant type, and must show that for any and with types as above, we have . By function extensionality, it suffices to show for all and . This follows from . ∎
A binary relation on a set is well-founded if every element of is accessible.
The point of well-foundedness is that for , we can use the induction principle of to conclude , and then apply well-foundedness to conclude . In other words, if from we can prove , then . This is called well-founded induction.
Well-foundedness is a mere property.
Well-foundedness of is the type , which is a mere proposition since each is. ∎
Perhaps the most familiar well-founded relation is the usual strict ordering on . To show that this is well-founded, we must show that is accessible for each . This is just the usual proof of “strong induction” from ordinary induction on .
Specifically, we prove by induction on that is accessible for all . The base case is just that is accessible, which is vacuously true since nothing is strictly less than . For the inductive step, we assume that is accessible for all , which is to say for all ; hence by definition is also accessible.
A different relation on which is also well-founded is obtained by setting only for all . Well-foundedness of this relation is almost exactly the ordinary induction principle of .
Let and be a family of sets. Recall from \autorefsec:w-types that the -type is inductively generated by the single constructor
We define the relation on by recursion on its second argument:
For any and , we define to mean that there merely exists a such that .
Now we prove that every is accessible for this relation, using the usual induction principle for . This means we assume given and , and also a lifting . But then by definition of , we have for all ; hence is accessible.
Suppose is a set and we have a function
Then if is a well-founded relation on , there is a function such that for all we have
(We are using the notation for images of subsets from \autorefsec:image.)
We first define, for every and , an element . By induction, it suffices to assume that is a function assigning to each a witness , and that moreover for each such we have an element . In this case, we define
Now since is well-founded, we have a function . Thus, we can define . ∎
In classical logic, well-foundedness has a more well-known reformulation. In the following, we say that a subset is nonempty if it is unequal to the empty subset . We leave it to the reader to verify that assuming excluded middle, this is equivalent to mere inhabitation, i.e. to the condition .
Assuming excluded middle, is well-founded if and only if every nonempty subset merely has a minimal element.
Suppose first is well-founded, and suppose is a subset with no minimal element. That is, for any with , there merely exists a with and .
We claim that for any and , we have . By induction, we may assume is a function assigning to each a proof , and that moreover for each such we have . If , then by assumption, there would merely exist a with , which contradicts this assumption. Thus, ; this completes the induction. Since is well-founded, we have for all , i.e. is empty.
Now suppose each nonempty subset merely has a minimal element. Let . Then if is nonempty, it merely has a minimal element. Thus there merely exists an with such that for all , we have . But then by definition (and induction on truncation), is merely accessible, and hence accessible, contradicting . Thus, is empty, so is well-founded. ∎
A well-founded relation on a set is extensional if for any , we have
Note that since 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.
The type of extensional well-founded relations is a set.
By the univalence axiom, it suffices to show that if is extensional and well-founded and , then . We prove by induction on that for all . The inductive hypothesis is that for all , we have .
If and are extensional and well-founded, a simulation is a function such that
if , then , and
for all and , if , then there merely exists an with .
Any simulation is injective.
We prove by double well-founded induction that for any , if then . The inductive hypothesis for says that for any , and any , if then . The inner inductive hypothesis for says that for any , if then .
In particular, this implies that in \autorefdef:simulation2 the word “merely” could be omitted without change of sense.
If is a simulation, then for all and , if , there purely exists an with .
Since is injective, is a mere proposition. ∎
We say that a subset is an initial segment if and imply . 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 is equal to the inclusion of some initial segment of .
For a set , let be the type of extensional well-founded relations on . If and and , let be the mere proposition that is a simulation. Then is a standard notion of structure over in the sense of \autorefsec:sip.
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 are two extensional well-founded relations on , and is a simulation in both directions, then and are equal. Since extensionality and well-foundedness are mere propositions, for this it suffices to have . But this follows from \autorefdef:simulation1 for . ∎
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.
For extensional and well-founded and , there is at most one simulation .
Suppose are simulations. Since being a simulation is a mere property, it suffices to show . By induction on , we may suppose for all . And by extensionality of , to have it suffices to have .
But since is a simulation, if , then we have with . By the inductive hypothesis, we have also , hence . The dual argument is symmetrical. ∎
Thus, if and are equipped with extensional and well-founded relations, we may write to mean there exists a simulation . \autorefthm:wfcat implies that if and , then .
Of course, the usual strict order on 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 order. We now show that also admits a well-founded relation.
If is an ordinal and , let denote the initial segment. Note that if as ordinals, then that isomorphism must respect their inclusions into (since simulations form a poset), and hence they are equal as subsets of . Therefore, since is extensional, . Thus the function is an injection .
For ordinals and , a simulation is said to be bounded if there exists such that .
The remarks above imply that such a is unique when it exists, so that boundedness is a mere property.
We write if there exists a bounded simulation from to . Since simulations are unique, is also a mere proposition.
is an ordinal.
Let be an ordinal; we first show that is accessible (in ) for all . By well-founded induction on , suppose is accessible for all . By definition of accessibility, we must show that is accessible in for all . However, if then there is some such that , which is accessible by the inductive hypothesis. Thus, is accessible for all .
Now to show that is accessible in , by definition we must show is accessible for all . But as before, means for some , which is accessible as we just proved. Thus, is well-founded.
For extensionality, suppose and are ordinals such that Then for every , since , we have , hence there is with . Define to take each to the corresponding ; it is straightforward to verify that is an isomorphism. Thus , hence 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.
Let be a universe. For any , there is a such that .
Let , with the element being greater than all elements of . Then is an ordinal and it is easy to see that . ∎
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 if and only if for some . This gives an isomorphism , so that . Thus we may take . ∎
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.
Similar remarks apply to the next lemma, which could be proved in a less useful way by observing that for any .
Let be a universe. For any and , there exists such that for all .
|Title||10.3 Ordinal numbers|