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.

The operation of cardinal addition

(\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.

There is an injection $A\to B$ .
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