(defaxiom succ
"The successor integer."
[]
(==> int int))
A computer language is not just a way of getting a computer to perform operations but rather that it is a novel formal medium for expressing ideas about methodology. Thus, programs must be written for people to read, and only incidentally for machines to execute. - Preface, SICP 1st Ed. https://mitpress.mit.edu/sicp/front/node3.html
this is recursive, which is just how a function like succ works (with a bit more work, anyway) but the definition rather concernes a polymorph function.
You do work in a particular encoding when you mention yero, at least. and succ^x is also an encoding (where x is zero or succ^y, where y is zero or ...).
That encoding is completely opaque, though. You have no way of knowing what are the members of zero.
The main difference between type theories and set theories is that type theories have particular syntactic discipline. Everything else is or can be a feature of set theories, too.
It is true that the fact that "there exists" (in a very nonconstructive sense) some unknowable, impenetrable encoding may offend the aesthetical sensibilities of some people, but type theory does not really "resolve" that in any way (and it is certainly not superior, just different, or rather, it is superior in some ways and inferior in others[2]); it simply constructs its axioms at a higher level of abstraction. The axiomatic existence of inductive data types in type theory is just a theorem about well-founded sets in set theory, but those sets are really defined in exactly the same abstract way.
[1]: So the natural numbers can be defined as "epsilon set N, s.t. N is the minimal set s.t. an element zero exists in N and there exists a function succ in the set N -> N, such that for all n in N, succ(n) is in n, and there is no n in N s.t. succ(n) = zero".
[2]: For example, because most type theories are based on the lambda calculus, they are on the precipice of inconsistency due to Curry's paradox, which makes some aspects of working with them extremely unpleasant compared to set theory.