1
$\begingroup$

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?

$\endgroup$
4
  • 2
    $\begingroup$ If "intuitionistic type theory" means something like the internal logic of topoi, then, even though it doesn't have dependent types as a primitive construction, it can define them in terms of its own primitive concepts. $\endgroup$
    – Andreas Blass
    Sep 24, 2020 at 20:44
  • $\begingroup$ Yes, in Part 2 of Introduction to higher order categorical logic it is shown that intuitionistic type theory corresponds to toposes in the sense that there is an adjunction between the category of intuitionistic type theories and the category of toposes, one functor sending a topos to its internal language. How can dependent types be defined in the internal language of toposes? $\endgroup$
    – user828672
    Sep 24, 2020 at 20:57
  • 2
    $\begingroup$ The details are a bit tedious (e.g., to handle contexts properly), but the basic idea is that a dependent type $A(x)$ indexed over a type $B$ is just a morphism $X\to B$, whose fibers are the $A(x)$'s. The sum of this dependent family would just be $X$; the non-trivial thing is to define dependent products. This is probably done by Lambek & Scott, perhaps under the heading of "locally cartesian closed"; it's surely in Freyd's paper "Aspects of topoi" and Johnstone's book "Topos theory". $\endgroup$
    – Andreas Blass
    Sep 24, 2020 at 21:08
  • $\begingroup$ I can't find the discussion in Freyd's paper "Aspects of topoi". He doesn't seem to talk about internal logics at all. Also, how can you consider a dependent type $(A_x)_{x\colon B}$ as a morphism $A\colon X\to B$? The fibers will be subsets of $X$, i.e., elements of the type $PX$. Intuitionistic type theory, as described by Lambek and Scott, has no mechanism to consider an element of type $PX$ as a type itself. $\endgroup$
    – user828672
    Sep 26, 2020 at 16:37

1 Answer 1

Reset to default
1
$\begingroup$

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.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .