Why is intuitionistic type theory without dependent types more powerful than Martin-Löf type theory? In the preface of Introduction to higher order categorical logic, Lambek and Scott write (emphasis mine):

[L]ogicians have made three attempts to formulate higher order logic, in increasing power: typed $\lambda$-calculus, Martin-Löf type theory and the usual (let us say intuitionistic) type theory.

What they call 'intuitionistic type theory' is defined in Part 2 of the book. What I find confusing: according to their definition, an intuitionistic type theory doesn't have dependent types. So how can 'intuitionistic type theory' be more powerful than Martin-Löf type theory?
 A: The somewhat more detailed version of things (which I'm not sure will fit in the comments) goes roughly like this:
The fibers of the map $A : X → B$ will be disjoint subsets of $X$, so $X$ is meant to be the disjoint union of all the sets $A_x$. This means that the fiber over $x$ in this disjoint union is equivalent to the $A_x$ set.
The type theoretic disjoint union operation $Σ_{x:B} A_x$ is accomplished by composition with the map to the terminal object, which gives a map $X → 1$, which can be interpreted as a single type.
Picking out a particular fiber into a type by itself is accomplished by pulling back $A : X → B$ along an element $x : 1 → B$.
Π types are related to sections. I believe the way to see this is that $Π_{x:B}$ is right adjoint to the pullback operation along $! : B → 1$. This means that there is a correspondence between elements: $$\hat f : 1 → Π_{x:B}A_x$$ and sections:
$$
\require{AMScd}
\begin{CD}
B @>{f}>>X \\
@V{id}VV @VVV \\
B @= B
\end{CD}
$$
in the over category.
Anyhow, all these decodings can be accomplished by talking about equality of non-dependent types, although it may not be pleasant to think in terms of the decoded propositions.
As far as "power" goes, I would imagine that that is due to toposes having a subobject classifier $Ω$, while Martin-löf type theory does not (although there are examples of dependent type theories with one). This gives you power sets/types, and considerably increases the power over a comparable theory without them.
