Is there a definition of what is a 'free monoid' which does not pre-suppose that the natural numbers has already been defined? The definitions that I have been able to track down all use the natural numbers (since sequences/words need them).

In other words, I am trying to define the theory of free monoids (as a signature with sorts, operations and axioms), and I would like to know if I can do this without having the theory of the naturals already defined. For exhibiting/constructing a free monoid, I do expect to need Nat.

Note that my ambient logic is higher-order, so I am fine with a second-order axiomatization. If dependent-types are needed, that would also be acceptable.

Is there a definition of what is a 'free monoid' which does not pre-suppose that the natural numbers has already been defined? The definitions that I have been able to track down all use the natural numbers (since sequences sequences/words need them).

In other words, I am trying to define the theory of free monoids (as a signature with sorts, operations and axioms), and I would like to know if I can do this without having the theory of the naturals already defined. For exhibiting/constructing a free monoid, I do expect to need Nat.

Is there a definition of a 'free monoid' which does not pre-suppose that the natural numbers has already been defined? The definitions that I have been able to track down all use the natural numbers (since sequences need them).

In other words, I am trying to define the theory of free monoids (as a signature with sorts, operations and axioms), and I would like to know if I can do this without having the theory of the naturals already defined.