Why is intuitionistic type theory without dependent types more powerful than Martin-Löf type theory?

419 Views Asked by At

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?

1

There are 1 best solutions below

0
On BEST ANSWER

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.