Definition 1.8.2.2. We define:

Crd :=: {|*S*| | *S* is a set}

|*S*| = |*T*| :⇔ ∃ *f* : *S* ↔ *T* (*S* is a set, *T* is a set)

We write “let *κ* be a cardinal number” for “let *κ* ∈ Crd.”

Remarks.

In HLM, cardinal numbers have a very simple definition as a construction with one constructor, which can be conveniently equipped with a notation that matches mathematical practice.

Given that two arbitrary sets cannot be compared element-wise due to the type system, the equality definition for cardinal numbers is the most general definition possible: No other valid equality definition can possibly distinguish two equipollent sets. This implies that definitions involving the "deconstruction" of cardinal numbers into sets are automatically well-defined.

HLM does not distinguish between sets and proper classes; instead there are rules preventing certain circularities. Thus, the set of cardinals can be treated like any other set in most situations.

When defining a construction, an embedding from another set into the newly defined set can be specified, subject to a suitable well-definedness condition. Embedding the natural numbers in the cardinal numbers simplifies a lot of definitions and theorems (see `$finite`

, `$"Cardinality of power set"`

).

In a way, the definition of cardinal numbers in HLM is very similar to the definition of algebraic structures (see e.g. `$../../../Algebra/"Pointed sets"/"Pointed sets"`

, `$../../../Algebra/Magmas/Magmas`

, `$../../../Algebra/Groups/Groups`

). This is especially visible in the use of this definition in the category of sets `$../../../"Category theory"/"Concrete categories"/cardinals`

.

References.