nLab
relation between type theory and category theory

under construction

Idea

type theory? and certain kinds of category theory are closely related. One may view type theory as a formal syntactic language or calculus for category theory, and conversely one may think of category theory as providing semantics for type theory. The flavor of category theory used depends on the flavor of type theory; this also extends to homotopy type theory and certain kind sof (∞,1)-category theory.

Overview

flavor of type theory	$$equivalent to$$	flavor of category theory
intuitionistic propositional logic?/simply-typed lambda calculus?		cartesian closed category
intuitionistic linear logic?		monoidal closed category
classical linear logic?		star-autonomous category
first-order logic		hyperdoctrine	(Seely 1984a)
Martin-Löf dependent type theory		locally cartesian closed category	(Seely 1984b)
homotopy type theory		locally cartesian closed (∞,1)-category	(conjectural)
homotopy type theory with higher inductive types and univalence		elementary (∞,1)-topos	(conjectural)

Theorems

We discuss here formalizations and proofs of the relation/equivalence between various flavors of type theories and the corresponding flavors of categories.

• First order logic and hyperdoctrines

• Martin-Löf Dependent type theory and locally cartesian closed categories

• Homotopy type theory and locally cartesian closed (∞,1)-categories

• Homotopy type theory with univalence and elementary (∞,1)-toposes

First-order logic and hyperdoctrines

Theorem

The functors

• $\mathrm{Cont}$, that form a category of contexts of a first-order theory;

• $\mathrm{Lang}$, that forms the internal language of a hyperdoctrine

constitute an equivalence of categories

$$\mathrm{FirstOrderTheories}\stackrel{\stackrel{\mathrm{Lang}}{\leftarrow }}{\underset{\mathrm{Cont}}{\to }}\mathrm{Hyperdoctrines}.$$FirstOrderTheories \stackrel{\overset{Lang}{\leftarrow}}{\underset{Cont}{\to}} Hyperdoctrines \,.

(Seely, 1984a)

Martin-Löf dependent type theory and locally cartesian closed categories

Theorem

There are 2-functors

• $\mathrm{Cont}$, that forms a category of contexts of a Martin-Löf dependent type theory;

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

that constitute an equivalence of 2-categories

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

This was originally claimed as an equivalence of categories (Seely, theorem 6.3). However, that argument did not properly treat a subtlety central to the whole subject: that substitution of terms for variables composes strictly, while its categorical semantics by pullback is by the very nature of pullbacks only defined up to isomorphism. This problem was pointed out and ways to fix it were given in (Curien) and (Hofmann); see categorical model of dependent types for the latter. However, the full equivalence of categories was not recovered until (Clairambault-Dybjer) solved both problems by promoting the statement to an equivalence of 2-categories.

We now indicate some of the details.

Type theories

For definiteness, self-containedness and for references below, we say what a dependent type theory is, following (Seely, def. 1.1).

Definition

A Martin-Löf dependent type theory $T$ is a theory with some signature of dependent function symbols with values in types and in terms (…) subject to the following rules

1. type formation rules

   1. $1$ is a type (the unit type);

   2. if $a,b$ are terms of type $A$, then $(a=b)$ is a type (the equality type);

   3. if $A$ and $B[x]$ are types, $B$ depending on a free variable of type $A$, then the following symbols are types

      1. ${\prod }_{a:A}B[a]$ (dependent product), written also $(A\to B)$ if $B[x]$ in fact does not depend on $x$;

      2. ${\sum }_{a:A}B[a]$ (dependent sum), written also $A\times B$ if $B[x]$ in fact does not depend on $x$;

2. term formation rules

   1. $*\in 1$ is a term of the unit type;

   2. (…)

3. equality rules

   1. (…)

Category of contexts

Definition

Given a dependent type theory $T$, its category of contexts $\mathrm{Con}(T)$ is the category whose

• objects are the types of $T$;

• morphisms $f:A\to B$ are the terms $f$ of function type $A\to B$.

Composition is given in the evident way.

Proposition

$\mathrm{Con}(T)$ has finite limits and is a cartesian closed category.

(Seely, prop. 3.1)

Proof

Constructions are straightforward. We indicated some of them.

Notice that all finite limits (as discussed there) are induced as soon as there are all pullbacks and equalizers. A pullback in $\mathrm{Con}(T)$

$$\begin{array}{ccc}P& \to & A\\ \downarrow & & {\downarrow }^f\\ B& \stackrel{g}{\to }& C\end{array}$$\array{ P &\to& A \\ \downarrow && \downarrow^{\mathrlap{f}} \\ B &\stackrel{g}{\to}& C }

is given by

$$P\simeq \sum _{a:A}\sum _{b\in B}(f(a)=g(b)).$$P \simeq \sum_{a : A} \sum_{b \in B} (f(a) = g(b)) \,.

The equalizer

$$P\to A\stackrel{\stackrel{f}{\to }}{\underset{g}{\to }}B$$P \to A \stackrel{\overset{f}{\to}}{\underset{g}{\to}} B

is given by

$$P=\sum _{a:A}(f(a)=g(a)).$$P = \sum_{a : A} (f(a) = g(a)) \,.

Next, the internal hom/exponential object is given by function type

$$[A,B]\simeq (A\to B).$$[A,B] \simeq (A \to B) \,.

Proposition

$\mathrm{Con}(T)$ is a locally cartesian closed category.

(Seely, theorem 3.2)

Proof

Define the $\mathrm{Con}(T)$-indexed hyperdoctrine $P(T)$ by taking for $A\in \mathrm{Con}(T)$ the category $P(T)(A)$ to have as objects the $A$-dependent types and as morphisms $(a:A⊢X(a):\mathrm{type})\to (a:A⊢Y(a):\mathrm{type})$ the terms of dependent function type $(a:A⊢t:(X(a)\to Y(a)))$.

This is cartesian closed by the same kind of argument as in the previous proof. It is now sufficient to exhibit a compatible equivalence of categories with the slice category $\mathrm{Con}(T{)}_{/A}$.

$$\mathrm{Con}(T{)}_{/A}\simeq P(T)(A).$$Con(T)_{/A} \simeq P(T)(A) \,.

In one direction, send a morphism $f:X\to A$ to the dependent type

$$a:A⊢f^{-1}(a)≔\sum _{x:X}(a=f(x)).$$a : A \vdash f^{-1}(a) \coloneqq \sum_{x : X} (a = f(x)) \,.

Conversely, for $a:A⊢X(a)$ a dependent type, send it to the projection ${\sum }_{a:A}X(a)\to A$.

One shows that this indeed gives an equivalence of categories which is compatible with base change (Seely, prop. 3.2.4).

Definition

For $T$ a dependent type theory and $C$ a locally cartesian closed category, an interpretation of $T$ in $C$ is a morphism of locally cartesian closed categories

$$\mathrm{Con}(T)\to C.$$Con(T) \to C \,.

An interpretation of $T$ in another dependent type theory $T\prime$ is a morphism of locally cartesian closed categories

$$\mathrm{Con}(T)\to \mathrm{Con}(T\prime ).$$Con(T) \to Con(T') \,.

Internal language

Proposition

Given a locally cartesian closed category $C$, define the corresponding dependent type theory $\mathrm{Lang}(C)$ as follows

• the non-dependent types of $\mathrm{Lang}(C)$ are the objects of $C$;

• the $A$-dependent types are the morphisms $B\to A$;

• a context $x_1:X,x_2:X,\cdots ,x_n:X_n$ is a tower of morphisms

  $$\begin{array}{c}{X}_n\\ \downarrow \\ \cdots \\ \downarrow \\ X_2\\ \downarrow \\ X_1\end{array}$$\array{ X_n \\ \downarrow \\ \cdots \\ \downarrow \\ X_2 \\ \downarrow \\ X_1 }

• the terms $t[x_A]:B[x_A]$ are the sections $A\to B$ in $C_{/A}$

• the equality type $(x_A=y_A)$ is the diagonal $A\to A\times A$

• …

Homotopy type theory and locally cartesian closed $(\mathrm{\infty },1)$-categories

(…)

Homotopy type theory with univalence and elementary $(\mathrm{\infty },1)$-toposes

(…)

Related concepts

• categorical model of dependent types

• computational trinitarianism

References

The equivalence of categories between first order theories and hyperdoctrines is discussed in

• R. A. G. Seely, Hyperdoctrines, natural deduction, and the Beck condition, Zeitschrift für Math. Logik und grundlagen der Math. (1984) (pdf)

A lecture reviewing aspects involved in this equivalence is (see the discussion building up to the theorem on slide 96)

• Tom Hirschowitz, Introduction to categorical logic (2010) (pdf)

An adjunction between the category of type theories with product types and toposes is discussed in chapter II of

• Joachim Lambek, P. Scott, Introduction to higher order categorical logic, Cambridge University Press (1986) .

The equivalence of categories between locally cartesian closed categories and dependent type theories was originally claimed in

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

following a statement earlier conjectured in

• Per Martin-Löf, An intuitionistic theory of types: predicative part, In Logic Colloquium (1973), ed. H. E. Rose and J. C. Shepherdson (North-Holland, 1974), 73-118.

The problem with strict substitution compared to weak pullback in this argument was discussed and fixed in

• Pierre-Louis Curien, Substitution up to isomorphism, Fundamenta Informaticae, 19(1,2):51–86 (1993)

• Martin Hofmann, _ On the interpretation of type theory in locally cartesian closed categories_, Proc. CSL ‘94, Kazimierz, Poland. Jerzy Tiuryn and Leszek Pacholski, eds. Springer LNCS, Vol. 933 (CiteSeer)

but in the process the equivalence of categories was lost. This was finally all rectified in

• Pierre Clairambault, Peter Dybjer, The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theories (arXiv:1112.3456)

The analogous statement relating homotopy type theory and locally cartesian closed (infinity,1)-categories was conjectured around

• André Joyal, Remarks on homotopical logic, Oberwolfach (2011) (pdf)

The suggestion that with univalence this is refined to (∞,1)-topos theory appears around

• Steve Awodey, Type theory and homotopy (pdf)

A precise definition of elementary (infinity,1)-topos inspired by giving a natural equivalence to homotopy type theory with univalence was then proposed in

• Mike Shulman, Inductive and higher inductive types (2012) (pdf)

A discussion of the correspondence between type theories and categories of various sorts, from lex categories to toposes is in

• Maria Emilia Maietti, Modular correspondence between dependent type theories and categories including pretopoi and topoi, Math. Struct. in Comp. Science (2005), vol. 15, pp. 1089–1149 (gzipped ps) (doi)