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 \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 theory	category theory
syntax	semantics
judgment	diagram
type	object in category
$\vdash\; A \; \mathrm{type}$	$A \in \mathcal{C}$
term	element
$\vdash\; a \colon A$	$* \stackrel{a}{\to} A$
dependent type	object in slice category
$x \colon X \;\vdash\; A(x) \; \mathrm{type}$	$\array{A \\ \downarrow \\ X} \in \mathcal{C}_{/X}$
term in context	generalized 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

• $Cont$, that form a category of contexts of a dependent type theory;

• $Lang$ that forms the internal language of a locally cartesian closed category

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.

Examples

• objective type theory
• book HoTT
• Martin-Löf type theory
• cubical type theory
• higher observational type theory
• univalent type theory
• propositional logic as a dependent type theory

Related concepts

• categorical semantics of dependent types

  relation between category theory and type theory

• linear dependent type theory

• set theory and dependent type theory

• dependent type theoretic methods in natural language semantics

References

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

• Martin Hofmann, Syntax and semantics of dependent types, Chapter 2 in: Extensional concepts in intensional type theory, Ph.D. thesis, University of Edinburgh (1995), Distinguished Dissertations, Springer (1997) [ECS-LFCS-95-327, pdf, doi:10.1007/978-1-4471-0963-1]

also published as:

• Martin Hofmann, Syntax and semantics of dependent types, in Semantics and logics of computation, Publ. Newton Inst. 14, Cambridge Univ. Press (1997) 79-130 [doi:10.1017/CBO9780511526619.004]

Gentle exposition of the basic principles:

• Thomas Kehrenberg, Introduction to dependent type theory (2022-23) [blog series]

Introductory accounts:

• Simon Thompson, §6.3 in: Type Theory and Functional Programming, Addison-Wesley (1991) [ISBN:0-201-41667-0, webpage, pdf]

• Bart Jacobs, Chapter 10 in: Categorical Logic and Type Theory, Studies in Logic and the Foundations of Mathematics 141, Elsevier (1998) [ISBN:978-0-444-50170-7, pdf]

  (emphasis on the categorical model of dependent types)

Introduction with parallel details on using proof assistants:

for Coq:

• Adam Chlipala, Certified programming with dependent types, MIT Press 2013 [ISBN:9780262026659, pdf, book webpage]

• Théo Winterhalter, Formalisation and Meta-Theory of Type Theory, Nantes (2020) [pdf, github]

for Agda:

• Ulf Norell, Dependently Typed Programming in Agda, p. 230-266 in: Advanced Functional Programming AFP 2008. Lecture Notes in Computer Science 5832 (2009) [doi:10.1007/978-3-642-04652-0_5, pdf]

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

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:

• Andrej Bauer, Philipp G. Haselwarter, Peter LeFanu Lumsdaine, A general definition of dependent type theories [arXiv:2009.05539]

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

• Egbert Rijke, An algebraic formulation of dependent type theory, (mailing list discussion)
• Vladimir Voevodsky, B-systems, (arXiv:1410.5389)
• Vladimir Voevodsky, A C-system defined by a universe in a category, (arXiv:1406.7413)
• Vladimir Voevodsky, C-system of a module over a monad on sets, (arXiv:1406.7413)
• Vladimir Voevodsky, Subsystems and regular quotients of C-systems, (arXiv:1406.7413)

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