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.