Definition 1.8.2.4.1.  Let κ, μ be cardinal numbers. We define:
Hom(κ, μ) := ((κ) → (μ))
We write “let φ:κ → μ be a homomorphism” for “let φ ∈ Hom(κ, μ).”
Remarks.

The definition of cardinal numbers in HLM is very similar to the definition of algebraic structures such as magmas. Thus it makes sense to define a homomorphism between cardinal numbers as a function between representative sets.

Although these sets are not unique, the type system prevents the ambiguities that could arise, as long as the equality definition of the structure does not define any non-isomorphic elements as equal.

References.