Contents

Contents

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 \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 theorycategory theory
syntaxsemantics
judgmentdiagram
typeobject in category
$\vdash\; A \colon Type$$A \in \mathcal{C}$
termelement
$\vdash\; a \colon A$$* \stackrel{a}{\to} A$
dependent typeobject in slice category
$x \colon X \;\vdash\; A(x) \colon Type$$\array{A \\ \downarrow \\ X} \in \mathcal{C}_{/X}$
term in contextgeneralized elements/element in slice category
$x \colon X \;\vdash \; a(x)\colon A(x)$$\array{X &&\stackrel{a}{\to}&& A \\ & {}_{\mathllap{id_X}}\searrow && \swarrow_{\mathrlap{}} \\ && X}$
$x \colon X \;\vdash \; a(x)\colon A$$\array{X &&\stackrel{(id_X,a)}{\to}&& X \times A \\ & {}_{\mathllap{id_X}}\searrow && \swarrow_{\mathrlap{p_1}} \\ && X}$

Properties

Theorem

The functors

constitute an equivalence of categories

$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.

References

All the essential ingredients are listed in

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