# What categories correspond to the typed lambda calculus with parametric types?

the unadorned typed lambda calculus correspond to the closed cartesian categories, but if we add in dependent or parametric types how are they then characterised?

-

Dependent type theory, i.e., $\lambda$-calculus with dependent products and dependent sums corresponds to locally cartesian closed categories, which was written up by R. Seely in "Locally cartesian closed categories and type theory", Math. Proc. Phil. Comb. Soc, (1984), 95, 33.
The internal language of a locally Cartesian closed category is a dependent type theory. A category $\mathcal C$ is locally Cartesian closed, if all of its slices $\mathcal C/X$ are Cartesian closed. An arrow $f:X\to Y$ is both interpreted as a variable substitution and as a family of types indexed over $Y$ in the type theory.