I am not sure whether the following comment points in the right direction. Anyway, have a look at https://en.wikipedia.org/wiki/Church_encoding and Barendregt's book as well as his article in the handbook of logic in computer science.

In general, one can introduce new types as an abbreviation of an existing set of other types in the type universe. Of course, there are many ways how this can be done. In higher order logic theorem provers that is usually done by such a type together with two functions that translate the new type into the available one and back. That is defined in more detail in Tom Melham's paper:

T. Melham, ‘Automating Recursive Type Definitions in Higher Order Logic’, in Current Trends in Hardware Verification and Automated Theorem Proving, edited by G. Birtwistle and P. A. Subrahmanyam (Springer-Verlag, 1989), pp. 341–386.

It is clearly required that the two sets in question have the same cardinality which gives you a first hint on how to select a suitable set. In that way, all types like booleans, natural numbers, integers, lists, sets, reals, etc. are defined on top of a basic set of individuals which is an unspecified infinite type that builds up the semantic universe of a higher order logic. Again Melham's paper above shows some of these constructions.

For primitive recursive types, there is a recipe for a type definition. Melham's achievement was to automate the definition of primitive recursive types in higher order logic which you can find in the above paper so that users of the theorem prover just have to list the primitive recursive definition, and Melham's procedure automatically implemented its embedding in the existing types.

Note that once you have natural numbers, Gödelization allows one to embed also other data types. That is typically not comfortable, so that is why Melham's work abstracts from that and introduces new types. Church initiated such encodings that are nowadays also used in higher order logic theorem provers.