Can we prove the Peano axioms from a type theoretic construction of the natural numbers? Here are two quotes that, while not literally contradictory, reach conclusions that are opposite in spirit.
The first one states that the Peano axioms can be proven to hold for an explicit construction of the Natural numbers in set theory:
Wikipedia states:

The Peano axioms can be derived from set theoretic constructions of the natural numbers and axioms of set theory such as ZF.

The second one states that at least one of the axioms (induction) cannot be proven to hold for an explicit construction of the natural numbers in type theory.
Nederpelt & Geuvers (Type theory and formal proof, an introduction. p. 306) state:

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. Hence, we need an extra axiom to represent it.

What explains this difference? 
Set theory and type theory are both proposed as a "foundation of mathematics". Based on my naive perspective, these two quotes seem to suggest that there is an important difference between the two, as foundations of mathematics. Is this intuition correct?
Is there a way to "solve" this, by somehow extending type theory, or something like that, so that the peano axioms can be proven true for some construction of the naturals in type theory?
 A: 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. 
