nLab
dependent type theory

Idea

Dependent type theory is the flavor of type theory that admits dependent types.

Its categorical semantics is in locally cartesian closed categories $C$, where a dependent type

$$x:X⊢E(x):\mathrm{Type}$$x : X \vdash E(x) : Type

is interpreted as a morphism $E\to X$, hence an object in the slice category $C_{/X}$.

Then change of context corresponds to base change in $C$. See also dependent sum and dependent product.

Dependent type systems are heavily used for software certification.

They also seem to support a foundations of mathematics in terms of homotopy type theory.

Description

Judgments for types and terms

type theory	category theory
syntax	semantics
judgment	diagram
type	object in category
$⊢A:\mathrm{Type}$	$A\in 𝒞$
term	element
$⊢a:A$	$*\stackrel{a}{\to }A$
dependent type	object in slice category
$x:X⊢A(x):\mathrm{Type}$	$\begin{array}{c}A\\ \downarrow \\ X\end{array}\in {𝒞}_{/X}$
term in context	generalized elements/element in slice category
$x:X⊢a(x):A(x)$	$\begin{array}{ccccc}X& & \stackrel{a}{\to }& & A\\ & {}_{{\mathrm{id}}_X}\searrow & & {\swarrow }_{}\\ & & X\end{array}$
$x:X⊢a(x):A$	$\begin{array}{ccccc}X& & \stackrel{({\mathrm{id}}_X,a)}{\to }& & X\times A\\ & {}_{{\mathrm{id}}_X}\searrow & & {\swarrow }_{p_1}\\ & & X\end{array}$

Properties

Theorem

The functors

• $\mathrm{Cont}$, that form a category of contexts of a dependent type theory;

• $\mathrm{Lang}$ that forms the internal language of a locally cartesian closed category

constitute an equivalence of categories

$$\mathrm{DependentTypeTheories}\stackrel{\stackrel{\mathrm{Lang}}{\leftarrow }}{\underset{\mathrm{Cont}}{\to }}\mathrm{LocallyCartesianClosedCategories}.$$DependentTypeTheories \stackrel{\overset{Lang}{\leftarrow}}{\underset{Cont}{\to}} LocallyCartesianClosedCategories \,.

This (Seely, theorem 6.3). It is somewhat more complicated than this, because we need to strictify the category theory to match the category theory; see categorical model of dependent types. For a more detailed discussion see at relation between type theory and category theory.

Examples

• Martin-Löf dependent type theory.

References

All the essential ingredients are listed in

• Nicola Gambino, Lectures on dependent type theory (pdf)

In part I there the standard type formation, term introduction/term elimination and computation rules of dependent type theory are listed.

An introduction with parallel details on Coq-programming is in

• Adam Chlipala, Certified programming with dependent types

See also

• Agda Tutorial: Introduction to dependent type theory (webpage)

A discussion of dependent type theory as the internal language of locally cartesian closed categories is in

• R. A. G. Seely, Locally cartesian closed categories and type theory, Math. Proc. Camb. Phil. Soc. (1984) 95 (pdf)

For more see the references at Martin-Löf dependent type theory.