10.2 Cardinal numbers

Definition 10.2.1.

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


Thus, a cardinal number, or cardinal, is an inhabitant of Card≑βˆ₯\setβˆ₯0. Technically, of course, there is a separate type CardU associated to each universePlanetmathPlanetmath U.

As usual for truncations, if A is a set, then |A|0 denotes its image under the canonical projection \setβ†’βˆ₯\setβˆ₯0≑𝖒𝖺𝗋𝖽; we call |A|0 the cardinality of A. By definition, 𝖒𝖺𝗋𝖽 is a set. It also inherits the structureMathworldPlanetmath of a semiring from \set.

Definition 10.2.2.

The operationMathworldPlanetmath of cardinal additionMathworldPlanetmath


is defined by inductionMathworldPlanetmath on truncation:


Since 𝖒𝖺𝗋𝖽→𝖒𝖺𝗋𝖽 is a set, to define (Ξ±+–):𝖒𝖺𝗋𝖽→𝖒𝖺𝗋𝖽 for all Ξ±:𝖒𝖺𝗋𝖽, by induction it suffices to assume that Ξ± is |A|0 for some A:\set. Now we want to define (|A|0+–):𝖒𝖺𝗋𝖽→𝖒𝖺𝗋𝖽, i.e.Β we want to define |A|0+Ξ²:𝖒𝖺𝗋𝖽 for all Ξ²:𝖒𝖺𝗋𝖽. However, since 𝖒𝖺𝗋𝖽 is a set, by induction it suffices to assume that Ξ² is |B|0 for some B:\set. But now we can define |A|0+|B|0 to be |A+B|0. ∎

Definition 10.2.3.

Similarly, the operation of cardinal multiplication


is defined by induction on truncation:

Lemma 10.2.4.

𝖒𝖺𝗋𝖽 is a commutativePlanetmathPlanetmathPlanetmathPlanetmath semiring, i.e.Β for Ξ±,Ξ²,Ξ³:Card we have the following.

(Ξ±+Ξ²)+Ξ³ =Ξ±+(Ξ²+Ξ³)
Ξ±+0 =Ξ±
Ξ±+Ξ² =Ξ²+Ξ±
(Ξ±β‹…Ξ²)β‹…Ξ³ =Ξ±β‹…(Ξ²β‹…Ξ³)
Ξ±β‹…1 =Ξ±
Ξ±β‹…Ξ² =Ξ²β‹…Ξ±
Ξ±β‹…(Ξ²+Ξ³) =Ξ±β‹…Ξ²+Ξ±β‹…Ξ³

where 0:≑|0|0 and 1:≑|1|0.


We prove the commutativity of multiplication, Ξ±β‹…Ξ²=Ξ²β‹…Ξ±; the others are exactly analogous. Since 𝖒𝖺𝗋𝖽 is a set, the type Ξ±β‹…Ξ²=Ξ²β‹…Ξ± is a mere proposition, and in particular a set. Thus, by induction it suffices to assume Ξ± and Ξ² are of the form |A|0 and |B|0 respectively, for some A,B:\set. Now |A|0β‹…|B|0≑|AΓ—B|0 and |B|0Γ—|A|0≑|BΓ—A|0, so it suffices to show AΓ—B=BΓ—A. Finally, by univalence, it suffices to give an equivalence AΓ—B≃BΓ—A. But this is easy: take (a,b)↦(b,a) and its obvious inverseMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath. ∎

Definition 10.2.5.

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

Lemma 10.2.6.

For Ξ±,Ξ²,Ξ³:Card we have

Ξ±0 =1
1Ξ± =1
Ξ±1 =Ξ±
Ξ±Ξ²+Ξ³ =Ξ±Ξ²β‹…Ξ±Ξ³
Ξ±Ξ²β‹…Ξ³ =(Ξ±Ξ²)Ξ³
(Ξ±β‹…Ξ²)Ξ³ =Ξ±Ξ³β‹…Ξ²Ξ³

Exactly like \autorefcard:semiring. ∎

Definition 10.2.7.

The relationMathworldPlanetmathPlanetmath of cardinal inequality


is defined by induction on truncation:


where inj⁒(A,B) is the type of injections from A to B. In other words, |A|0≀|B|0 means that there merely exists an injection from A to B.

Lemma 10.2.8.

Cardinal inequality is a preorderMathworldPlanetmath, i.e.Β for Ξ±,Ξ²:Card we have


As before, by induction on truncation. For instance, since (α≀β)β†’(β≀γ)β†’(α≀γ) is a mere proposition, by induction on 0-truncation we may assume Ξ±, Ξ², and Ξ³ are |A|0, |B|0, and |C|0 respectively. Now since |A|0≀|C|0 is a mere proposition, by induction on (-1)-truncation we may assume given injections f:Aβ†’B and g:Bβ†’C. But then g∘f is an injection from A to C, so |A|0≀|C|0 holds. ReflexivityMathworldPlanetmath 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→B.

  2. 2.

    There is a surjection B→A.

Then, assuming excluded middle:

  • β€’

    Given a0:A, we haveΒ 1β†’2.

  • β€’

    Therefore, if A is merely inhabited, we haveΒ 1 β†’ merely 2.

  • β€’

    Assuming the axiom of choiceMathworldPlanetmath, we haveΒ 2 β†’ merely 1.


If f:Aβ†’B is an injection, define g:Bβ†’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):≑a; otherwise set g(b):≑a0. 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β†’A is surjective, then by the axiom of choice, there merely exists a function f:Aβ†’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


The usual β€œback-and-forth” argument applies without significant changes. Note that it actually constructs an isomorphismPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath Aβ‰…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 orderMathworldPlanetmath, i.e.Β for Ξ±,Ξ²:Card we have


Since Ξ±=Ξ² is a mere proposition, by induction on truncation we may assume Ξ± and Ξ² are |A|0 and |B|0, respectively, and that we have injections f:Aβ†’B and g:Bβ†’A. But then the Schroeder–Bernstein theorem gives an isomorphism A≃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:\set, there is no surjection A→(A→2).


Suppose f:Aβ†’(Aβ†’πŸ) is any function, and define g:Aβ†’πŸ by g(a):≑¬f(a)(a). If g=f⁒(a0), then g⁒(a0)=f⁒(a0)⁒(a0) but g⁒(a0)=¬⁒f⁒(a0)⁒(a0), a contradictionMathworldPlanetmathPlanetmath. Thus, f is not surjective. ∎

Corollary 10.2.13.

Assuming excluded middle, for any Ξ±:Card, there is a cardinal Ξ² such that α≀β and Ξ±β‰ Ξ².


Let Ξ²=2Ξ±. Now we want to show a mere proposition, so by induction we may assume Ξ± is |A|0, so that β≑|Aβ†’πŸ|0. Using excluded middle, we have a function f:Aβ†’(Aβ†’πŸ) defined by

f(a)(aβ€²):≑{1𝟐a=aβ€²0𝟐aβ‰ aβ€².

And if f⁒(a)=f⁒(aβ€²), then f⁒(aβ€²)⁒(a)=f⁒(a)⁒(a)=1𝟐, so a=aβ€²; hence f is injective. Thus, α≑|A|0≀|Aβ†’πŸ|0≑2Ξ±.

On the other hand, if 2α≀α, then we would have an injection (Aβ†’πŸ)β†’A. By \autorefthm:injsurj, since we have (λ⁒x⁒. 0𝟐):Aβ†’πŸ and excluded middle, there would then be a surjection Aβ†’(Aβ†’πŸ), contradicting Cantor’s theorem. ∎

Title 10.2 Cardinal numbers