Peano axioms come to model the natural numbers, and their most important property: the fact we can use induction on the natural numbers. This has nothing to do with set theory. Equally one can talk about the axioms of a real-closed field, or a vector space.
Axioms are given to give a definition for a mathematical object. It is a basic setting from which we can prove certain propositions.
As it turns out, however, it is possible to use the natural numbers as a basis for some of our mathematics, and we can use Peano axioms to model first-order logic (its syntax and the inference rules), and the notion of a proof.
This can be seen as a basis for some of the mathematics we do, however it is often a syntactical basis only: we only use the integers to manipulate strings in our language and sequences of these strings. We do not have the notion of a structure, of a model.
But it seems that you are mainly confused by the use of the term "axioms". These are just basic properties for a mathematical object. In this case "the natural numbers". Much like there are axioms in geometry, but geometry doesn't usually serve as a basis for many parts in mathematics.
First off, the distinction you're attempting to between "counting numbers" and "natural numbers" doesn't match how the words is usually used in mathematics. To a mathematician, "the natural numbers" in general means the pre-formal concept you're calling "counting numbers". (And the phrasing "counting numbers" generally isn't used at all). In particular, being a model of this or that formal system doesn't qualify anything as being the natural numbers; only the true Platonic natural numbers are natural numbers.
(That's except for people who have learned enough set theory to know how natural numbers are usually modeled there, but haven't yet gained a sufficiently wide horizon on the matter to know that the model is not the actual thing).
Whether the natural numbers are a human invention or not is something of a philosophical morass that I won't go into -- but the mere fact that they were not created by Peano is not a controversial statement.
Now, since we understand the naturals intuitively, at least to a pretty good extent, what do we need axioms for? Well, most primitively, to see how well we can do by reasoning purely mechanically from axioms. For example, it led to a significant improvement in geometrical reasoning when the ancient Greeks started demanding rigorous proofs from axioms rather than just geometrical intuition; it is natural to wish to know whether something similar could be done for arithmetic.
As it happens, it took many centuries after the Greeks before formal mathematical reasoning had progressed enough that it was thinkable that it might be possible to reason about integer arithmetic without depending on intuition. Peano's axioms were not aimed at telling anything new about the integers -- he was simply one of the first to have a sufficiently well developed notion of formal logic that he could hope to make an axiomatic treatment of the integers work.
The goal of the investigation, then, is not primarily to discover something new about the integers themselves, but to see whether a formal system can be made to support a "mechanical" reasoning about them that is rich and strong to conclude what we already know about them intuitively.
The Peano axioms (and their modern first-order successor, Peano Arithmetic) were somewhat successful in that, but nonetheless the crowning achievement of the whole program turned out to be a negative result: Gödel's Incompleteness Theorem tells us that every reasonable formal system for proving things about the integers will be incomplete: there are truths about the natural numbers that it cannot prove.
Nevertheless, it is still interesting in itself to investigate the strength and properties of various such formal systems.
Also, of course, it is pragmatically useful that when something can be proved in a formal system with few axioms to it, then it is very certain to be true about the actual naturals ... there's a much smaller risk of having overlooked something during the proof than if we base our reasoning purely on an intuitive understanding of how the naturals ought to behave. In this way it's kind of a gold standard for a proof that it can (in principle) be reduced to Peano Arithmetic or a similarly bare-bones system. We recognize that there will be things that can't, but these exceptions will be subject to a lot more scrutiny before one considers oneself convinced that they are in fact true.
Best Answer
The quote from Nederpelt & Geuvers in the question has been abridged. They actually write:
A key point here is that the authors are discussing Church numerals in particular. The second half of p. 305 and the top half of p. 306 are devoted to explaining why the natural numbers should not be formalized as Church numerals in the systems they have described. After that discussion, they go on to formalize the integers and natural numbers in a different way.
On p. 313, after formalizing the naturals and integers, they write:
There is no contradiction. On one hand, they don't use Church numerals. The more important point is that they assume various axioms about the integers, in their Figure 14.3, and construct the natural numbers as predicate on the integers.
There are interesting differences between type theory and set theory. They approach mathematics from almost opposite perspectives (essentially: highly typed versus completely untyped). But both type theory and set theory can produce foundational systems strong enough for practical use in formalizing everyday mathematics, including the Peano postulates.
Of course it is necessary to include enough axioms in either kind of theory to prove the results that you are interested in. In set theory, this assumption takes the form of the "axiom of infinity", without which ZFC set theory cannot prove there is any infinite set. In type theory, we will also need an axiom showing there is a type with an infinite number of elements, and with appropriate functions. The axioms in Figure 14.3 are one way to achieve this.
As a follow up: the OP is asking why is appears that type theory "explicitly" assumes the induction principle for $N$, while set theory "proves" it. However, this is just an artifact of the way that set theory and type theory quantify over predicates. If we use a somewhat unnatural definition of $N$ in type theory, we can mimic the same kind of definition as in set theory.
In set theory, we use the axiom of infinity and a set existence axiom to produce a set $\omega$ which is the smallest set containing $0$ and closed under the operation $\operatorname{succ}\colon x \mapsto \{x\} \cup x$. In particular, letting $I$ be the set from the axiom of infinity, we define $$ \omega = \bigcap \{ S \subseteq I : 0 \in S \land (\forall x)[x \in S \to \operatorname{succ}(x) \in S\}. $$ Here, the quantifier is over all subsets $S\subseteq I$, rather than over all "properties". Interestingly, this is a kind of impredicative definition: the set $\omega$ itself is one of the candidates for $S$ in the intersection.
With this definition, the "second order" induction axiom $$ 0 \in S \land (\forall n \in N)[n \in S \to n+1 \in S) \to (\forall m)[m \in S] $$ follows immediately from the definition of $\omega$.
In type theory, we will similarly need some axioms to assert the existence of a type $N$ that contains an initial element $0$ and is inductively generated by a function $s\colon N \to N$. The issue is how to formalize "is inductively generated by" within type theory. Of course, part of being "inductively generated" is that, for every $f \colon N \to \{T, F\}$, if $f(0)$ and $(\forall n:N)[ fn \to f(n+1)]$ then $(\forall k:N) fk$. The authors state this as the 'axiom of induction'.
If we insisted, in type theory we could instead mimic the set theoretic definition of $N$ by defining a function $g \colon N \to \{T,F\}$ by $$ gk \leftrightarrow (\forall f \colon N \to \{T,F\})[f0 \land (\forall m : N)[fm \to f(m+1)] \to fk]$$ This is also an impredicative definition: $g$ itself is a candidate for $f$. With that definition, we could let $N'$ be the subset of $N$ defined the predicate $g$, and we could prove that induction holds for $N'$, immediately from the definition of $g$. However, that is not the way that type theory is normally used, because it misses the spirit of type theory.
The axiom of induction for $N$ is better viewed as a basic axiom of type theory - it is simply the way that type theory expresses the inductive construction of $N$ from $0$ and $s$. We would have a similar induction axiom for any inductively defined type, so we are not really assuming anything about $N$ beyond what would normally be assumed about an inductively defined type.
Analogously, the general set existence axioms in set theory allow us to form subsets of $N$, but we don't view them as special assumptions about the natural numbers - the set existence axioms are just part of set theory, just as induction principles for inductively defined types are part of type theory.