10.2 Cardinal numbers

Definition 10.2.1.

The type of cardinal numbersis the 0-truncation of the type of sets:

$$\mathrm{𝖢𝖺𝗋𝖽}:\equiv \parallel {\parallel }_0$$

Thus, a cardinal number, or cardinal, is an inhabitant of $\mathrm{Card}\mathrm{\equiv }\mathrm{\parallel }{\mathrm{\parallel }}_{\mathrm{0}}$.Technically, of course, there is a separate type ${\mathrm{Card}}_{\mathrm{U}}$ associated to each universe $\mathrm{U}$.

As usual for truncations, if $A$ is a set, then ${\left|A\right|}_0$ denotes its image under the canonical projection $\to \parallel {\parallel }_0\equiv \mathrm{𝖢𝖺𝗋𝖽}$; we call ${\left|A\right|}_0$ the cardinality of $A$.By definition, $\mathrm{𝖢𝖺𝗋𝖽}$ is a set.It also inherits the structure of a semiring from .

Definition 10.2.2.

The operation of cardinal addition

$$(\mathit{\text{–}}+\mathit{\text{–}}):\mathrm{𝖢𝖺𝗋𝖽}\to \mathrm{𝖢𝖺𝗋𝖽}\to \mathrm{𝖢𝖺𝗋𝖽}$$

is defined by induction on truncation:

$$|A{|}_0+|B{|}_0:\equiv |A+B{|}_0.$$

Proof.

Since $\mathrm{𝖢𝖺𝗋𝖽}\to \mathrm{𝖢𝖺𝗋𝖽}$ is a set, to define $(\alpha +\text{–}):\mathrm{𝖢𝖺𝗋𝖽}\to \mathrm{𝖢𝖺𝗋𝖽}$ for all $\alpha :\mathrm{𝖢𝖺𝗋𝖽}$, by induction it suffices to assume that $\alpha$ is ${\left|A\right|}_0$ for some $A:$.Now we want to define $(|A{|}_0+\text{–}):\mathrm{𝖢𝖺𝗋𝖽}\to \mathrm{𝖢𝖺𝗋𝖽}$, i.e. we want to define $|A{|}_0+\beta :\mathrm{𝖢𝖺𝗋𝖽}$ for all $\beta :\mathrm{𝖢𝖺𝗋𝖽}$.However, since $\mathrm{𝖢𝖺𝗋𝖽}$ is a set, by induction it suffices to assume that $\beta$ is ${\left|B\right|}_0$ for some $B:$.But now we can define $|A{|}_0+|B{|}_0$ to be ${\left|A+B\right|}_0$.∎

Definition 10.2.3.

Similarly, the operation of cardinal multiplication

$$(\mathit{\text{–}}\cdot \mathit{\text{–}}):\mathrm{𝖢𝖺𝗋𝖽}\to \mathrm{𝖢𝖺𝗋𝖽}\to \mathrm{𝖢𝖺𝗋𝖽}$$

is defined by induction on truncation:

$$|A{|}_0\cdot |B{|}_0:\equiv |A\times B{|}_0$$

Lemma 10.2.4.

$\mathrm{𝖢𝖺𝗋𝖽}$ is a commutative semiring, i.e. for $\alpha \mathrm{,}\beta \mathrm{,}\gamma \mathrm{:}\mathrm{Card}$ we have the following.

$(\alpha +\beta )+\gamma$$=\alpha +(\beta +\gamma )$

$\alpha +0$$=\alpha$

$\alpha +\beta$$=\beta +\alpha$

$(\alpha \cdot \beta )\cdot \gamma$$=\alpha \cdot (\beta \cdot \gamma )$

$\alpha \cdot 1$$=\alpha$

$\alpha \cdot \beta$$=\beta \cdot \alpha$

$\alpha \cdot (\beta +\gamma )$$=\alpha \cdot \beta +\alpha \cdot \gamma$

where $\mathrm{0}\mathrm{:}\mathrm{\equiv }\mathrm{|}\mathrm{0}{\mathrm{|}}_{\mathrm{0}}$ and $\mathrm{1}\mathrm{:}\mathrm{\equiv }\mathrm{|}\mathrm{1}{\mathrm{|}}_{\mathrm{0}}$.

Proof.

We prove the commutativity of multiplication, $\alpha \cdot \beta =\beta \cdot \alpha$; the others are exactly analogous.Since $\mathrm{𝖢𝖺𝗋𝖽}$ 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 ${\left|A\right|}_0$ and ${\left|B\right|}_0$ respectively, for some $A,B:$.Now $|A{|}_0\cdot |B{|}_0\equiv |A\times B{|}_0$ and $|B{|}_0\times |A{|}_0\equiv |B\times A{|}_0$, 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:

$${|A{|}_0}^{|B{|}_0}:\equiv |B\to A{|}_0.$$

Lemma 10.2.6.

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

${\alpha }^0$$=1$

$1^{\alpha }$$=1$

${\alpha }^1$$=\alpha$

${\alpha }^{\beta +\gamma }$$={\alpha }^{\beta }\cdot {\alpha }^{\gamma }$

${\alpha }^{\beta \cdot \gamma }$$={({\alpha }^{\beta })}^{\gamma }$

${(\alpha \cdot \beta )}^{\gamma }$$={\alpha }^{\gamma }\cdot {\beta }^{\gamma }$

Proof.

Exactly like card:semiring.∎

Definition 10.2.7.

The relation of cardinal inequality

$$(\mathit{\text{–}}\le \mathit{\text{–}}):\mathrm{𝖢𝖺𝗋𝖽}\to \mathrm{𝖢𝖺𝗋𝖽}\to \mathrm{𝖯𝗋𝗈𝗉}$$

is defined by induction on truncation:

$$|A{|}_0\le |B{|}_0:\equiv \parallel \mathrm{𝗂𝗇𝗃}(A,B)\parallel$$

where $\mathrm{inj}\mathit{}\mathrm{(}A\mathrm{,}B\mathrm{)}$ is the type of injections from $A$ to $B$.In other words, $\mathrm{|}A{\mathrm{|}}_{\mathrm{0}}\mathrm{\le }\mathrm{|}B{\mathrm{|}}_{\mathrm{0}}$ means that there merely exists an injection from $A$ to $B$.

Lemma 10.2.8.

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

$$\alpha \le \alpha$$

$$(\alpha \le \beta )\to (\beta \le \gamma )\to (\alpha \le \gamma )$$

Proof.

As before, by induction on truncation.For instance, since $(\alpha \le \beta )\to (\beta \le \gamma )\to (\alpha \le \gamma )$ is a mere proposition, by induction on 0-truncation we may assume $\alpha$, $\beta$, and $\gamma$ are ${\left|A\right|}_0$, ${\left|B\right|}_0$, and ${\left|C\right|}_0$ respectively.Now since $|A{|}_0\le |C{|}_0$ 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 $|A{|}_0\le |C{|}_0$ 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

$$\mathrm{𝗂𝗇𝗃}(A,B)\to \mathrm{𝗂𝗇𝗃}(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 \mathrm{,}\beta \mathrm{:}\mathrm{Card}$ we have

$$(\alpha \le \beta )\to (\beta \le \alpha )\to (\alpha =\beta ).$$

Proof.

Since $\alpha =\beta$ is a mere proposition, by induction on truncation we may assume $\alpha$ and $\beta$ are ${\left|A\right|}_0$ and ${\left|B\right|}_0$, 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 $|A{|}_0=|B{|}_0$.∎

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

Theorem 10.2.12 (Cantor).

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

Proof.

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

Corollary 10.2.13.

Assuming excluded middle, for any $\alpha \mathrm{:}\mathrm{Card}$, there is a cardinal $\beta$ such that $\alpha \mathrm{\le }\beta$ and $\alpha \mathrm{\ne }\beta$.

Proof.

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

And if $f(a)=f(a^{\prime })$, then $f(a^{\prime })(a)=f(a)(a)=1_{\mathrm{𝟐}}$, so $a=a^{\prime }$; hence $f$ is injective.Thus, $\alpha \equiv |A{|}_0\le |A\to \mathrm{𝟐}{|}_0\equiv 2^{\alpha }$.

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