HOL Light doesn't have subtyping. If the type system had subtyping, there would be terms that are assigned two different types, where one type is a subtype of t

HOL Light doesn't have subtyping. If the type system had subtyping, there would be terms that are assigned two different types, where one type is a subtype of the other. So, in a truly subtyped system, you would have it that 3 has both type N and type R, with N being a subtype of R. Instead, in HOL Light, there is a total function from N to R, and a partial function from R to N. HOL Light allows you to carve out new types of existing types using a predicate filter, and this is baked into the kernel in `fusion.ml`. But this doesn't introduce subtyping relations. Importantly, the kernel rule gives you abstraction and representation functions to move between elements of the new type and the original type, but, unlike in a subtyping system, the terms of the newly defined type are not simultaneously elements of the larger type.