# 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⊢E\left(x\right):\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 theorycategory theory
syntaxsemantics
judgmentdiagram
typeobject in category
$⊢\phantom{\rule{thickmathspace}{0ex}}A:\mathrm{Type}$$A\in 𝒞$
termelement
$⊢\phantom{\rule{thickmathspace}{0ex}}a:A$$*\stackrel{a}{\to }A$
dependent typeobject in slice category
$x:X\phantom{\rule{thickmathspace}{0ex}}⊢\phantom{\rule{thickmathspace}{0ex}}A\left(x\right):\mathrm{Type}$$\begin{array}{c}A\\ ↓\\ X\end{array}\in {𝒞}_{/X}$
term in contextgeneralized elements/element in slice category
$x:X\phantom{\rule{thickmathspace}{0ex}}⊢\phantom{\rule{thickmathspace}{0ex}}a\left(x\right):A\left(x\right)$$\begin{array}{ccccc}X& & \stackrel{a}{\to }& & A\\ & {}_{{\mathrm{id}}_{X}}↘& & {↙}_{}\\ & & X\end{array}$
$x:X\phantom{\rule{thickmathspace}{0ex}}⊢\phantom{\rule{thickmathspace}{0ex}}a\left(x\right):A$$\begin{array}{ccccc}X& & \stackrel{\left({\mathrm{id}}_{X},a\right)}{\to }& & X×A\\ & {}_{{\mathrm{id}}_{X}}↘& & {↙}_{{p}_{1}}\\ & & X\end{array}$

## Properties

###### Theorem

The functors

constitute an equivalence of categories

$\mathrm{DependentTypeTheories}\stackrel{\stackrel{\mathrm{Lang}}{←}}{\underset{\mathrm{Cont}}{\to }}\mathrm{LocallyCartesianClosedCategories}\phantom{\rule{thinmathspace}{0ex}}.$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