10.2 Cardinal numbers

Definition 10.2.1.

The type of cardinal numbers is the 0-truncation of the type \setof sets:

 $\mathsf{Card}:\!\!\equiv\mathopen{}\left\|\set\right\|_{0}\mathclose{}$

Thus, a cardinal number, or cardinal, is an inhabitant of $\mathsf{Card}\equiv\mathopen{}\left\|\set\right\|_{0}\mathclose{}$. Technically, of course, there is a separate type $\mathsf{Card}_{\mathcal{U}}$ associated to each universe $\mathcal{U}$.

As usual for truncations, if $A$ is a set, then $\mathopen{}\left|A\right|_{0}\mathclose{}$ denotes its image under the canonical projection $\set\to\mathopen{}\left\|\set\right\|_{0}\mathclose{}\equiv\mathsf{Card}$; we call $\mathopen{}\left|A\right|_{0}\mathclose{}$ the cardinality of $A$. By definition, $\mathsf{Card}$ is a set. It also inherits the structure of a semiring from \set.

Definition 10.2.2.

 $(\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}+\mathord{\hskip 1.0pt\text{--}% \hskip 1.0pt}):\mathsf{Card}\to\mathsf{Card}\to\mathsf{Card}$

is defined by induction on truncation:

 $\mathopen{}\left|A\right|_{0}\mathclose{}+\mathopen{}\left|B\right|_{0}% \mathclose{}:\!\!\equiv\mathopen{}\left|A+B\right|_{0}\mathclose{}.$
Proof.

Since $\mathsf{Card}\to\mathsf{Card}$ is a set, to define $(\alpha+\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}):\mathsf{Card}\to\mathsf{Card}$ for all $\alpha:\mathsf{Card}$, by induction it suffices to assume that $\alpha$ is $\mathopen{}\left|A\right|_{0}\mathclose{}$ for some $A:\set$. Now we want to define $(\mathopen{}\left|A\right|_{0}\mathclose{}+\mathord{\hskip 1.0pt\text{--}% \hskip 1.0pt}):\mathsf{Card}\to\mathsf{Card}$, i.e. we want to define $\mathopen{}\left|A\right|_{0}\mathclose{}+\beta:\mathsf{Card}$ for all $\beta:\mathsf{Card}$. However, since $\mathsf{Card}$ is a set, by induction it suffices to assume that $\beta$ is $\mathopen{}\left|B\right|_{0}\mathclose{}$ for some $B:\set$. But now we can define $\mathopen{}\left|A\right|_{0}\mathclose{}+\mathopen{}\left|B\right|_{0}% \mathclose{}$ to be $\mathopen{}\left|A+B\right|_{0}\mathclose{}$. ∎

Definition 10.2.3.

Similarly, the operation of cardinal multiplication

 $(\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\cdot\mathord{\hskip 1.0pt\text{--% }\hskip 1.0pt}):\mathsf{Card}\to\mathsf{Card}\to\mathsf{Card}$

is defined by induction on truncation:

 $\mathopen{}\left|A\right|_{0}\mathclose{}\cdot\mathopen{}\left|B\right|_{0}% \mathclose{}:\!\!\equiv\mathopen{}\left|A\times B\right|_{0}\mathclose{}$
Lemma 10.2.4.

$\mathsf{Card}$ is a commutative semiring, i.e. for $\alpha,\beta,\gamma:\mathsf{Card}$ we have the following.

 $\displaystyle(\alpha+\beta)+\gamma$ $\displaystyle=\alpha+(\beta+\gamma)$ $\displaystyle\alpha+0$ $\displaystyle=\alpha$ $\displaystyle\alpha+\beta$ $\displaystyle=\beta+\alpha$ $\displaystyle(\alpha\cdot\beta)\cdot\gamma$ $\displaystyle=\alpha\cdot(\beta\cdot\gamma)$ $\displaystyle\alpha\cdot 1$ $\displaystyle=\alpha$ $\displaystyle\alpha\cdot\beta$ $\displaystyle=\beta\cdot\alpha$ $\displaystyle\alpha\cdot(\beta+\gamma)$ $\displaystyle=\alpha\cdot\beta+\alpha\cdot\gamma$

where $0:\!\!\equiv\mathopen{}\left|\mathbf{0}\right|_{0}\mathclose{}$ and $1:\!\!\equiv\mathopen{}\left|\mathbf{1}\right|_{0}\mathclose{}$.

Proof.

We prove the commutativity of multiplication, $\alpha\cdot\beta=\beta\cdot\alpha$; the others are exactly analogous. Since $\mathsf{Card}$ is a set, the type $\alpha\cdot\beta=\beta\cdot\alpha$ is a mere proposition, and in particular a set. Thus, by induction it suffices to assume $\alpha$ and $\beta$ are of the form $\mathopen{}\left|A\right|_{0}\mathclose{}$ and $\mathopen{}\left|B\right|_{0}\mathclose{}$ respectively, for some $A,B:\set$. Now $\mathopen{}\left|A\right|_{0}\mathclose{}\cdot\mathopen{}\left|B\right|_{0}% \mathclose{}\equiv\mathopen{}\left|A\times B\right|_{0}\mathclose{}$ and $\mathopen{}\left|B\right|_{0}\mathclose{}\times\mathopen{}\left|A\right|_{0}% \mathclose{}\equiv\mathopen{}\left|B\times A\right|_{0}\mathclose{}$, so it suffices to show $A\times B=B\times A$. Finally, by univalence, it suffices to give an equivalence $A\times B\simeq B\times A$. But this is easy: take $(a,b)\mapsto(b,a)$ and its obvious inverse. ∎

Definition 10.2.5.

The operation of cardinal exponentiation is also defined by induction on truncation:

 $\mathopen{}\left|A\right|_{0}\mathclose{}^{\mathopen{}\left|B\right|_{0}% \mathclose{}}:\!\!\equiv\mathopen{}\left|B\to A\right|_{0}\mathclose{}.$
Lemma 10.2.6.

For $\alpha,\beta,\gamma:\mathsf{Card}$ we have

 $\displaystyle\alpha^{0}$ $\displaystyle=1$ $\displaystyle 1^{\alpha}$ $\displaystyle=1$ $\displaystyle\alpha^{1}$ $\displaystyle=\alpha$ $\displaystyle\alpha^{\beta+\gamma}$ $\displaystyle=\alpha^{\beta}\cdot\alpha^{\gamma}$ $\displaystyle\alpha^{\beta\cdot\gamma}$ $\displaystyle=(\alpha^{\beta})^{\gamma}$ $\displaystyle(\alpha\cdot\beta)^{\gamma}$ $\displaystyle=\alpha^{\gamma}\cdot\beta^{\gamma}$
Proof.

Exactly like \autorefcard:semiring. ∎

Definition 10.2.7.

The relation of cardinal inequality

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

is defined by induction on truncation:

 $\mathopen{}\left|A\right|_{0}\mathclose{}\leq\mathopen{}\left|B\right|_{0}% \mathclose{}:\!\!\equiv\mathopen{}\left\|\mathsf{inj}(A,B)\right\|\mathclose{}$

where $\mathsf{inj}(A,B)$ is the type of injections from $A$ to $B$. In other words, $\mathopen{}\left|A\right|_{0}\mathclose{}\leq\mathopen{}\left|B\right|_{0}% \mathclose{}$ means that there merely exists an injection from $A$ to $B$.

Lemma 10.2.8.

Cardinal inequality is a preorder, i.e. for $\alpha,\beta:\mathsf{Card}$ we have

 $\displaystyle\alpha\leq\alpha$ $\displaystyle(\alpha\leq\beta)\to(\beta\leq\gamma)\to(\alpha\leq\gamma)$
Proof.

As before, by induction on truncation. For instance, since $(\alpha\leq\beta)\to(\beta\leq\gamma)\to(\alpha\leq\gamma)$ is a mere proposition, by induction on 0-truncation we may assume $\alpha$, $\beta$, and $\gamma$ are $\mathopen{}\left|A\right|_{0}\mathclose{}$, $\mathopen{}\left|B\right|_{0}\mathclose{}$, and $\mathopen{}\left|C\right|_{0}\mathclose{}$ respectively. Now since $\mathopen{}\left|A\right|_{0}\mathclose{}\leq\mathopen{}\left|C\right|_{0}% \mathclose{}$ is a mere proposition, by induction on $(-1)$-truncation we may assume given injections $f:A\to B$ and $g:B\to C$. But then $g\circ f$ is an injection from $A$ to $C$, so $\mathopen{}\left|A\right|_{0}\mathclose{}\leq\mathopen{}\left|C\right|_{0}% \mathclose{}$ holds. Reflexivity is even easier. ∎

We may likewise show that cardinal inequality is compatible with the semiring operations.

Lemma 10.2.9.

Consider the following statements:

1. 1.

There is an injection $A\to B$.

2. 2.

There is a surjection $B\to A$.

Then, assuming excluded middle:

• Given $a_{0}:A$, we have 1$\to$2.

• Therefore, if $A$ is merely inhabited, we have 1 $\to$ merely 2.

• Assuming the axiom of choice, we have 2 $\to$ merely 1.

Proof.

If $f:A\to B$ is an injection, define $g:B\to A$ at $b:B$ as follows. Since $f$ is injective, the fiber of $f$ at $b$ is a mere proposition. Therefore, by excluded middle, either there is an $a:A$ with $f(a)=b$, or not. In the first case, define $g(b):\!\!\equiv a$; otherwise set $g(b):\!\!\equiv a_{0}$. Then for any $a:A$, we have $a=g(f(a))$, so $g$ is surjective.

The second statement follows from this by induction on truncation. For the third, if $g:B\to A$ is surjective, then by the axiom of choice, there merely exists a function $f:A\to B$ with $g(f(a))=a$ for all $a$. But then $f$ must be injective. ∎

Theorem 10.2.10 (Schroeder–Bernstein).

Assuming excluded middle, for sets $A$ and $B$ we have

 $\mathsf{inj}(A,B)\to\mathsf{inj}(B,A)\to(A\cong B)$
Proof.

The usual “back-and-forth” argument applies without significant changes. Note that it actually constructs an isomorphism $A\cong B$ (assuming excluded middle so that we can decide whether a given element belongs to a cycle, an infinite chain, a chain beginning in $A$, or a chain beginning in $B$). ∎

Corollary 10.2.11.

Assuming excluded middle, cardinal inequality is a partial order, i.e. for $\alpha,\beta:\mathsf{Card}$ we have

 $(\alpha\leq\beta)\to(\beta\leq\alpha)\to(\alpha=\beta).$
Proof.

Since $\alpha=\beta$ is a mere proposition, by induction on truncation we may assume $\alpha$ and $\beta$ are $\mathopen{}\left|A\right|_{0}\mathclose{}$ and $\mathopen{}\left|B\right|_{0}\mathclose{}$, respectively, and that we have injections $f:A\to B$ and $g:B\to A$. But then the Schroeder–Bernstein theorem gives an isomorphism $A\simeq B$, hence an equality $\mathopen{}\left|A\right|_{0}\mathclose{}=\mathopen{}\left|B\right|_{0}% \mathclose{}$. ∎

Finally, we can reproduce Cantor’s theorem, showing that for every cardinal there is a greater one.

Theorem 10.2.12 (Cantor).

For $A:\set$, there is no surjection $A\to(A\to\mathbf{2})$.

Proof.

Suppose $f:A\to(A\to\mathbf{2})$ is any function, and define $g:A\to\mathbf{2}$ by $g(a):\!\!\equiv\neg f(a)(a)$. If $g=f(a_{0})$, then $g(a_{0})=f(a_{0})(a_{0})$ but $g(a_{0})=\neg f(a_{0})(a_{0})$, a contradiction. Thus, $f$ is not surjective. ∎

Corollary 10.2.13.

Assuming excluded middle, for any $\alpha:\mathsf{Card}$, there is a cardinal $\beta$ such that $\alpha\leq\beta$ and $\alpha\neq\beta$.

Proof.

Let $\beta=2^{\alpha}$. Now we want to show a mere proposition, so by induction we may assume $\alpha$ is $\mathopen{}\left|A\right|_{0}\mathclose{}$, so that $\beta\equiv\mathopen{}\left|A\to\mathbf{2}\right|_{0}\mathclose{}$. Using excluded middle, we have a function $f:A\to(A\to\mathbf{2})$ defined by

 $f(a)(a^{\prime}):\!\!\equiv\begin{cases}{1_{\mathbf{2}}}&\quad a=a^{\prime}\\ {0_{\mathbf{2}}}&\quad a\neq a^{\prime}.\end{cases}$

And if $f(a)=f(a^{\prime})$, then $f(a^{\prime})(a)=f(a)(a)={1_{\mathbf{2}}}$, so $a=a^{\prime}$; hence $f$ is injective. Thus, $\alpha\equiv\mathopen{}\left|A\right|_{0}\mathclose{}\leq\mathopen{}\left|A\to% \mathbf{2}\right|_{0}\mathclose{}\equiv 2^{\alpha}$.

On the other hand, if $2^{\alpha}\leq\alpha$, then we would have an injection $(A\to\mathbf{2})\to A$. By \autorefthm:injsurj, since we have $({\lambda}x.\,{0_{\mathbf{2}}}):A\to\mathbf{2}$ and excluded middle, there would then be a surjection $A\to(A\to\mathbf{2})$, contradicting Cantor’s theorem. ∎

Title 10.2 Cardinal numbers
\metatable