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) \; \mathrm{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 \; \mathrm{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) \; \mathrm{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

For original references see at Martin-Löf dependent type theory, such as:

also published as:

Gentle exposition of the basic principles:

Introductory accounts:

Introduction with parallel details on using proof assistants:

for Coq:

for Agda:

Original 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)

A formal definition of dependent type theories beyond Martin-Löf dependent type theory:

On (essentially algebraic) formulations of dependent type theory (see here at categorical models of dependent type theory):

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

Last revised on February 4, 2023 at 13:13:39. See the history of this page for a list of all contributions to it.