10.4 Classical wellorderings
We now show the equivalence of our ordinals^{} with the more familiar classical wellorderings.
Lemma 10.4.1.
Assuming excluded middle, every ordinal is trichotomous:
$$ 
Proof.
By induction^{} on $a$, we may assume that for every $$ and every ${b}^{\prime}:A$, we have $$. Now by induction on $b$, we may assume that for every $$, we have $$.
By excluded middle, either there merely exists a $$ such that $$, or there merely exists a $$ such that $a={b}^{\prime}$, or for every $$ we have $$. In the first case, merely $$ by transitivity, hence $$ as it is a mere proposition. Similarly, in the second case, $$ by transport. Thus, suppose $$.
Now analogously, either there merely exists $$ such that $$, or there merely exists $$ such that ${a}^{\prime}=b$, or for every $$ we have $$. In the first and second cases, $$, so we may suppose $$. However, by extensionality, our two suppositions now imply $a=b$. ∎
Lemma 10.4.2.
A wellfounded relation contains no cycles, i.e.
$$ 
Proof.
In particular, a wellfounded relation must be irreflexive^{}, i.e. $$ for all $a$.
Theorem 10.4.3.
Assuming excluded middle, $$ is an ordinal if and only if every nonempty subset $B\mathrm{\subseteq}A$ has a least element.
Proof.
If $A$ is an ordinal, then by \autorefthm:wfmin every nonempty subset merely has a minimal element. But trichotomy implies that any minimal element is a least element. Moreover, least elements are unique when they exist, so merely having one is as good as having one.
Conversely, if every nonempty subset has a least element, then by \autorefthm:wfmin, $A$ is wellfounded. We also have trichotomy, since for any $a,b$ the subset $\text{setof}a,b:\equiv \text{setof}x:Ax=a\vee x=b$ merely has a least element, which must be either $a$ or $b$. This implies transitivity, since if $$ and $$, then either $a=c$ or $$ would produce a cycle. Similarly, it implies extensionality, for if $$, then $$ implies (letting $c$ be $a$) that $$, which is a cycle, and similarly if $$; hence $a=b$. ∎
In classical mathematics, the characterization of \autorefthm:wellorder is taken as the definition of a wellordering, with the ordinals being a canonical set of representatives of isomorphism classes for wellorderings. In our context, the structure^{} identity^{} principle means that there is no need to look for such representatives: any wellordering is as good as any other.
We now move on to consider consequences of the axiom of choice^{}. For any set $X$, let ${\mathcal{P}}_{+}(X)$ denote the type of merely inhabited subsets of $X$:
$${\mathcal{P}}_{+}(X):\equiv \text{setof}Y:\mathcal{P}(X)\exists (x:X).x\in Y.$$ 
Assuming excluded middle, this is equivalently the type of nonempty subsets of $X$, and we have $\mathcal{P}(X)\simeq ({\mathcal{P}}_{+}(X))+\mathrm{\U0001d7cf}$.
Theorem 10.4.4.
Assuming excluded middle, the following are equivalent^{}.

1.
For every set $X$, there merely exists a function $f:{\mathcal{P}}_{+}(X)\to X$ such that $f(Y)\in Y$ for all $Y:\mathcal{P}(X)$.

2.
Every set merely admits the structure of an ordinal.
Of course, 1 is a standard classical version of the axiom of choice; see \autorefex:choicefunction.
Proof.
One direction is easy: suppose 2. Since we aim to prove the mere proposition 1, we may assume $A$ is an ordinal. But then we can define $f(B)$ to be the least element of $B$.
Now suppose 1. As before, since 2 is a mere proposition, we may assume given such an $f$. We extend $f$ to a function
$$\overline{f}:\mathcal{P}(X)\simeq ({\mathcal{P}}_{+}(X))+\mathrm{\U0001d7cf}\u27f6X+\mathrm{\U0001d7cf}$$ 
in the obvious way. Now for any ordinal $A$, we can define ${g}_{A}:A\to X+\mathrm{\U0001d7cf}$ by wellfounded recursion:
$$ 
(regarding $X$ as a subset of $X+\mathrm{\U0001d7cf}$ in the obvious way).
Let ${A}^{\prime}:\equiv \text{setof}a:A{g}_{A}(a)\in X$ be the preimage^{} of $X\subseteq X+\mathrm{\U0001d7cf}$; then we claim the restriction^{} ${g}_{A}^{\prime}:{A}^{\prime}\to X$ is injective^{}. For if $a,{a}^{\prime}:A$ with $a\ne {a}^{\prime}$, then by trichotomy and without loss of generality, we may assume $$. Thus $$, so since $f(Y)\in Y$ for all $Y$ we have ${g}_{A}(a)\ne {g}_{A}({a}^{\prime})$.
Moreover, ${A}^{\prime}$ is an initial segment of $A$. For ${g}_{A}(a)$ lies in $\mathrm{\U0001d7cf}$ if and only if $$, and if this holds then it also holds for any ${a}^{\prime}>a$. Thus, ${A}^{\prime}$ is itself an ordinal.
Finally, since $\mathrm{\U0001d5ae\U0001d5cb\U0001d5bd}$ is an ordinal, we can take $A:\equiv \mathrm{\U0001d5ae\U0001d5cb\U0001d5bd}$. Let ${X}^{\prime}$ be the image of ${g}_{\mathrm{\U0001d5ae\U0001d5cb\U0001d5bd}}^{\prime}:{\mathrm{\U0001d5ae\U0001d5cb\U0001d5bd}}^{\prime}\to X$; then the inverse^{} of ${g}_{\mathrm{\U0001d5ae\U0001d5cb\U0001d5bd}}^{\prime}$ yields an injection $H:{X}^{\prime}\to \mathrm{\U0001d5ae\U0001d5cb\U0001d5bd}$. By \autorefthm:ordunion, there is an ordinal $C$ such that $Hx\le C$ for all $x:{X}^{\prime}$. Then by \autorefthm:ordsucc, there is a further ordinal $D$ such that $$, hence $$ for all $x:{X}^{\prime}$. Now we have
${g}_{\mathrm{\U0001d5ae\U0001d5cb\U0001d5bd}}(D)$  $$  
$=\overline{f}(X\setminus \text{setof}{g}_{\mathrm{\U0001d5ae\U0001d5cb\U0001d5bd}}(B){\text{}}{g}_{\mathrm{\U0001d5ae\U0001d5cb\U0001d5bd}}(B)\in X)$ 
since if $B:\mathrm{\U0001d5ae\U0001d5cb\U0001d5bd}$ and $({g}_{\mathrm{\U0001d5ae\U0001d5cb\U0001d5bd}}(B)\in X)$, then $B=Hx$ for some $x:{X}^{\prime}$, hence $$. Now if
$$\text{setof}{g}_{\mathrm{\U0001d5ae\U0001d5cb\U0001d5bd}}(B){\text{}}{g}_{\mathrm{\U0001d5ae\U0001d5cb\U0001d5bd}}(B)\in X$$ 
is not all of $X$, then ${g}_{\mathrm{\U0001d5ae\U0001d5cb\U0001d5bd}}(D)$ would lie in $X$ but not in this subset, which would be a contradiction^{} since $D$ is itself a potential value for $B$. So this set must be all of $X$, and hence ${g}_{\mathrm{\U0001d5ae\U0001d5cb\U0001d5bd}}^{\prime}$ is surjective as well as injective. Thus, we can transport the ordinal structure on ${\mathrm{\U0001d5ae\U0001d5cb\U0001d5bd}}^{\prime}$ to $X$. ∎
Remark 10.4.5.
If we had given the wrong proof of \autorefthm:ordsucc or \autorefthm:ordunion, then the resulting proof of \autorefthm:wop would be invalid: there would be no way to consistently assign universe^{} levels. As it is, we require propositional resizing (which follows from $\mathrm{LEM}$) to ensure that ${X}^{\mathrm{\prime}}$ lives in the same universe as $X$ (up to equivalence).
Corollary 10.4.6.
Assuming the axiom of choice, the function $\mathrm{Ord}\mathrm{\to}\text{set}$ (which forgets the order structure) is a surjection.
Note that $\mathrm{\U0001d5ae\U0001d5cb\U0001d5bd}$ is a set, while \setis a 1type. In general, there is no reason for a 1type to admit any surjective function from a set. Even the axiom of choice does not appear to imply that every 1type does so (although see \autorefex:acnmsurjset), but it readily implies that this is so for 1types constructed out of \set, such as the types of objects of categories of structures as in \autorefsec:sip. The following corollary also applies to such categories.
Corollary 10.4.7.
Assuming $\mathrm{AC}$, $\mathrm{S}\mathit{}e\mathit{}t$ admits a weak equivalence^{} functor from a strict category.
Proof.
Let ${X}_{0}:\equiv \mathrm{\U0001d5ae\U0001d5cb\U0001d5bd}$, and for $A,B:{X}_{0}$ let ${\mathrm{hom}}_{X}(A,B):\equiv (A\to B)$. Then $X$ is a strict category, since $\mathrm{\U0001d5ae\U0001d5cb\U0001d5bd}$ is a set, and the above surjection ${X}_{0}\to \text{set}$ extends to a weak equivalence functor $X\to \mathcal{S}et$. ∎
Now recall from \autorefsec:cardinals that we have a further surjection $\underset{\xaf}{}{}_{0}:\text{set}\to \mathrm{\U0001d5a2\U0001d5ba\U0001d5cb\U0001d5bd}$, and hence a composite surjection $\mathrm{\U0001d5ae\U0001d5cb\U0001d5bd}\to \mathrm{\U0001d5a2\U0001d5ba\U0001d5cb\U0001d5bd}$ which sends each ordinal to its cardinality.
Theorem 10.4.8.
Assuming $\mathrm{AC}$, the surjection $\mathrm{Ord}\mathrm{\to}\mathrm{Card}$ has a section^{}.
Proof.
There is an easy and wrong proof of this: since $\mathrm{\U0001d5ae\U0001d5cb\U0001d5bd}$ and $\mathrm{\U0001d5a2\U0001d5ba\U0001d5cb\U0001d5bd}$ are both sets, $\mathrm{\U0001d5a0\U0001d5a2}$ implies that any surjection between them merely has a section. However, we actually have a canonical specified section: because $\mathrm{\U0001d5ae\U0001d5cb\U0001d5bd}$ is an ordinal, every nonempty subset of it has a uniquely specified least element. Thus, we can map each cardinal to the least element in the corresponding fiber. ∎
It is traditional in set theory^{} to identify cardinals with their image in $\mathrm{\U0001d5ae\U0001d5cb\U0001d5bd}$: the least ordinal having that cardinality.
It follows that $\mathrm{\U0001d5a2\U0001d5ba\U0001d5cb\U0001d5bd}$ also canonically admits the structure of an ordinal: in fact, one isomorphic^{} to $\mathrm{\U0001d5ae\U0001d5cb\U0001d5bd}$. Specifically, we define by wellfounded recursion a function $\mathrm{\aleph}:\mathrm{\U0001d5ae\U0001d5cb\U0001d5bd}\to \mathrm{\U0001d5ae\U0001d5cb\U0001d5bd}$, such that $\mathrm{\aleph}(A)$ is the least ordinal having cardinality greater than $\mathrm{\aleph}({A}_{/a})$ for all $a:A$. Then (assuming $\mathrm{\U0001d5a0\U0001d5a2}$) the image of $\mathrm{\aleph}$ is exactly the image of $\mathrm{\U0001d5a2\U0001d5ba\U0001d5cb\U0001d5bd}$.
Title  10.4 Classical wellorderings 

\metatable 