Definition 1.8.2.2.  We define:
Crd:=: {|S| | S is a set}
|S| = |T|  :⇔    (S is a set, T is a set)
⊆:Crd vian = |<n|
Well-definedness.  Let m, n ∈  such that |<m| = |<n|. Then m = n:
|<m| = |<n|def
1.8.2.1 ⇒ m = n
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.