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.
The quote from Nederpelt & Geuvers in the question has been abridged. They actually write:
Firstly, it has been shown that induction, one of the most fundamental proof
principles of natural numbers, cannot be derived by means of the polymorphic Church numerals, not in λ2 or λP2 (Geuvers, 2001), and also not in λD. Hence, we need an extra axiom to represent it.
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:
Again, it is not necessary to formulate [induction for the natural numbers] as an extra axiom, because it is a theorem: it can be derived from our axioms for integers and the definition of N.
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.
Best Answer
No, the induction axiom does not construct the natural numbers, but in order for the induction axiom to hold (in addition to the other Peano Axioms), your model does need to be isomorph to the natural numbers. Indeed, it is almost the other way around: the induction axiom does not generate or construct or force there to be infinitely many ordered elements in any model, as this is what the other axioms already do, but rather the induction axiom makes sure that in any model there aren't any further elements. That is, the induction axiom restricts the model to be 'nothing more' than the natural numbers.
To give at least some intuitive idea about this: Any model of the Peano axioms without the induction axiom is already required to contain an infinite number of elements that exist somewhere in an infinite chain of successors starting with $0$, i.e. something like the natural numbers. To see that, note that we need a '$0$' object (axiom 1) and that this $0$ object needs a successor (Axiom 6), and that this successor of $0$ cannot be $0$ itself (Axiom 8). So, we need a second object. But this second object needs a successor (Axiom 6), which cannot be $0$ (Axiom 8), but also cannot be itself, for we cannot have two different objects with the same successor (Axiom 7). So, we need a third object ... and this process keeps repeating itself: every time we add the new object that we are forced to add as the successor of the last object we added before that, that new object needs a successor itself, and that successor cannot be $0$ (Axiom 8), nor can it be any of the other already existing objects, for then we would get two different objects with the same successor, which goes against Axiom 7. So, you could say that the natural numbers (or at least an infinite sequence of successive objects) is already 'constructed' by these 4 axioms.
OK, so where does the axiom of induction come in? Well, while the other axioms require for any model to contain an infinite sequence of successive element, these other axioms do not rule out any additional elements in the model: elements that do not occur in this infinite sequence of successors. Indeed, without the axiom of induction you could have as a model $\mathbb{N} \cup \{ apples, bananas \}$, ... as long as you define how the interpretation of the successor, addition and multiplication function symbols apply to $apples$ and $bananas$ ... but that can all be done without problem.
However, the induction axiom says that 'if $0$ has some property $P$, and if $s(n)$ has property $P$ whenever $n$ has property $P$, then all objects have property $P$. Well, if you have that $0$ has some property $P$, and that $s(n)$ has property $P$ whenever $n$ has property $P$, then obviously all the objects that exist somewhere in the infinite chain of successors have property $P$, but how can you say that all the additional objects also have to have property $P$? You can't of course. So, the fact that the induction axiom says that we can conclude that all objects have property $P$ effectively rules out any of those additional objects in the domain, and hence your model needs to be isomorph to the natural numbers.