nLab
categorical model of dependent types

Idea

In the relation between type theory and category theory, dependent types are said to correspond to morphisms regarded as indexed families. That is, if a type $A$ corresponds to an object in some category, then a dependent type

$$(x:A)⊢(B(x)\mathrm{type})$$(x:A) \;\vdash\; (B(x) \;type)

corresponds to a morphism $B\to A$ in that category. We think of this morphism as a bundle or fibration, whose fiber over $x:A$ is the type $B(x)$. We can then say that type forming operations such as dependent sum type and dependent product type correspond to category-theoretic operations of dependent sum and dependent product.

However, this correspondence is not quite precise; in the case of dependent types there are extra coherence issues. Substitution in type theory should correspond to pullback in category theory; that is, given a term

$$(y:C)⊢(f(y):A)$$(y:C) \;\vdash\; (f(y) : A)

corresponding to a morphism $f:C\to A$, the substituted dependent type

$$(y:C)⊢(B(f(y))\mathrm{type})$$(y:C) \;\vdash\; (B(f(y)) \;type)

should correspond to the pullback of $B\to A$ along $f$. However, substitution in type theory is strictly associative. That is, given also $g:D\to C$, the dependent type

$$(z:C)⊢(B(f(g(z)))\mathrm{type})$$(z:C) \;\vdash\; (B(f(g(z))) \;type)

is syntactically the same regardless of whether we obtain it by substituting $y≔g(z)$ into $B(f(y))$, or $x≔f(g(z))$ into $B(x)$. In category theory, however, pullback is not generally strictly associative, so there is a mismatch. Similarly, every type-forming operation must also be strictly preserved by substitition/pullback.

The way this is generally dealt with is to introduce a category-theoretic structure which does have a “substitution” operation which is strictly associative, hence does correspond directly to type theory, and then show that any category can be “strictified” into such a stricter structure. Unfortunately, there are many different such structures which have been used, differing only slightly. On this page we define and compare them all.

Definitions

In all the definitions, $C$ will be a category. Generally, we will regard the objects of $C$ as contexts in a type theory.

So far, we do not assume anything about $C$ as a category. Usually, one at least wants $C$ to have a terminal object, representing the empty context, although this is not always included in the definitions. The additional structures we impose on $C$ below will imply in particular that certain pullbacks exist in $C$.

Sometimes, we want to consider $C$ as a strict category, that is, we consider its objects up to equality rather than isomorphism. However, for most of the definitions below (until we get to contextual categories), it is still sensible to treat $C$ in an ordinary category-theoretic way, with the strictness living in the additional structure.

All of this could be made more precise by assembling the structures considered below into categories, 2-categories, and/or strict 2-categories.

Comprehension categories

Definition

A comprehension category consists of a commutative triangle of functors

$$\begin{array}{ccccc}E& & \to & & C^I\\ & \searrow & & \swarrow \\ & & C\end{array}$$\array{ E && \to && C^I\\ & \searrow && \swarrow\\ && C }

where $C^I$ is the arrow category of $C$, and such that

1. $E\to C$ is a Grothendieck fibration, and
2. $E\to C^I$ takes cartesian morphisms in $E$ to cartesian morphisms in $C^I$ (i.e. to pullback squares in $C$).

Remark

We do not ask that $C^I\to C$ be a fibration (that would require $C$ to have all pullbacks), only that the particular morphisms in the image of $E$ are cartesian.

Definition

A comprehension category is called

• full if $E\to C^I$ is a fully faithful functor.

• split if $E\to C$ is a split fibration.

Remark

In the latter case, we must consider $E$ at least to be a strict category (that is, we consider its objects up to equality rather than isomorphism) for the notion to make sense.

Remark

The interpretation of this definition is as follows.

In a comprehension category, we may regard the objects of $C$ as contexts, and the fiber $E^{\Gamma }$ of $E\to C$ over an object $\Gamma$ as the category of dependent types in context $\Gamma$. If the comprehension category is split, then such dependent types have strictly associative substitution.

The functor $E\to C^I$ assigns to each “type $A$ in context $\Gamma$” a new context which we think of as $\Gamma$ extended by a fresh variable of type $A$, and write as $\Gamma .A$. This new context $\Gamma .A$ comes with a projection $\Gamma .A\to \Gamma$ (which forgets the fresh variable), and all substitutions in $E$ are realized as pullbacks in $C$.

Display map categories

Definition

A display map category consists of a category $C$ together with a class $D$ of morphisms in $C$ called display maps, such that all pullbacks of display maps exist and are display maps.

If $C$ is a display map category, then by defining $E$ to be the full subcategory of $C^I$ whose objects are display maps, we obtain a full comprehension category. Thus, we have:

Lemma

Display map categories may be identified with comprehension categories, def. 1, for which the functor $E\to C^I$ is the inclusion of a full subcategory.

Remark

Working up to equivalence of categories, as is usual in category theory, it is natural to consider display map categories to also be equivalent to full comprehension categories, def. 2, (those where $E\to C^I$ is merely fully faithful).

However, this breaks down when we are interested in split comprehension categories, def. 2, for modeling substitution with strict associativity, since then $E$ at least must be regarded as a strict category and considered up to isomorphism rather than equivalence. Thus, display map categories may be said to be equivalent to non-split full comprehension categories, but “split display map categories” are not equivalent to split full comprehension categories. (In fact, split display map categories are not very useful; usually in order to make pullbacks strictly associative we have to introduce extra “names” for the same objects.)

Categories with attributes

Definition

A category with attributes is a comprehension category, def. 1, for which $E\to C$ is a discrete fibration.

Remark

That is, in a category with attributes we demand only that each context comes with a set of dependent types in that context, rather than a category of such. The intent is that the morphisms between two types in context $\Gamma$ should be determined by the morphisms in $C$ between the extended contexts over $\Gamma$.

Another way to convey this same intent with a comprehension category would be to ask that it be full, def. 2, i.e. that the functor $E\to C^I$ be fully faithful.

In fact, any category with attributes gives rise to a full comprehension category by factoring the functor $E\to C^I$ into a bijective on objects functor followed by a fully faithful one. In this way, we obtain:

Lemma

Categories with attributes, def. 4, are equivalent to full split comprehension categories, def. 2.

Categories with families

A category with attributes specifies only for each “context”, a set of “types” in that context. A comprehension category, by contrast, specifies a whole category of “types” in each context. If $A,B\in E^{\Gamma }$, then we can think of a morphism $f:A\to B$ in $E^{\Gamma }$ as a term

(1)$$(\stackrel{\rightharpoonup }{x}:\Gamma ),(a:A(\stackrel{\rightharpoonup }{x}))⊢(f(\stackrel{\rightharpoonup }{x},a):B(\stackrel{\rightharpoonup }{x}))$$(\vec{x} : \Gamma), (a:A(\vec{x})) \;\vdash\; (f(\vec{x},a) : B(\vec{x}))

in type theory.
A category with families specifies instead, for each context and each type in that context, a set of “terms belonging to that type”. These should be thought of as terms

(2)$$(\stackrel{\rightharpoonup }{x}:\Gamma )⊢(f(\stackrel{\rightharpoonup }{x}):B(\stackrel{\rightharpoonup }{x}))$$(\vec{x} : \Gamma) \;\vdash\; (f(\vec{x}) : B(\vec{x}))

in type theory.

Remark

A term of the form (1) can equivalently be regarded as a term of the form (2) by replacing $\Gamma$ by the extended context $\Gamma .A$, and $B$ by its substitution along the projection $\Gamma .A\to \Gamma$.

The additional insight in the following definition is that if we expect all of these terms to be determined by the morphisms in $C$, as in a category with attributes or a full comprehension category, then instead of specifying the functor $E\to C^I$ and then asking either that it be fully faithful or that $E$ be discrete (removing the information about extra morphisms in $E$), if we specify the terms of the form (2), then the functor $E\to C^I$ is determined by a universal property.

Let $\mathrm{Fam}$ denote the category of families of sets. Its morphisms are set-indexed families $(A_i{)}_{i\in I}$, and its morphisms $(A_i{)}_{i\in I}\to (B_j{)}_{j\in J}$ consist of a function $f:I\to J$ and functions $g_j:A_i\to B_{f(i)}$. We can equivalently, of course, regard this as the arrow category ${\mathrm{Set}}^I$ of Set, where $(A_i{)}_{i\in I}$ corresponds to the arrow $\coprod A\to I$.

Definition

A category with families is a category $C$ together with

• A functor $F:C^{\mathrm{op}}\to \mathrm{Fam}$, written $F(\Gamma )=(\mathrm{Tm}(A){)}_{A\in \mathrm{Ty}(\Gamma )}$.

• For each $\Gamma \in C$ and $A\in \mathrm{Ty}(\Gamma )$, a representing object for the functor

  $$\begin{array}{rl}(C/\Gamma {)}^{\mathrm{op}}& \to \mathrm{Set}\\ (\Delta \stackrel{f}{\to }\Gamma )& \mapsto \mathrm{Tm}(f^{*}(A))\end{array}$$\begin{aligned} (C/\Gamma)^{op} & \to Set\\ (\Delta \xrightarrow{f} \Gamma) & \mapsto Tm(f^*(A)) \end{aligned}

We can then prove:

Lemma

Categories with attributes, def. 4 are equivalent to categories with families, def. 5.

Proof

If we forget the terms in a category with families and let $E\to C$ be the Grothendieck construction of the functor $\mathrm{Ty}:C^{\mathrm{op}}\to \mathrm{Set}$, it is easy to show that we obtain a category with attributes. Conversely, given a category with attributes, let $\mathrm{Ty}:C^{\mathrm{op}}\to \mathrm{Set}$ be the functor corresponding to the discrete fibration $E\to C$, and for $A\in \mathrm{Ty}(\Gamma )$ let $\mathrm{Tm}(A)$ be the set of sections of the morphism in $C$ that is the image of $A$ in $C^I$. These constructions are inverses up to isomorphism.

The following alternative characterization was observed by Steve Awodey.

Theorem

If we modify Def. 5 by requiring only that the functors $(\Delta \stackrel{f}{\to }\Gamma )\mapsto \mathrm{Tm}(f^{*}(A))$ be representable (rather than equipped with representing objects), then it is equivalent to giving

1. a category $C$, together with
2. a morphism $\mathrm{Tm}\to \mathrm{Ty}$ in the category of presheaves on $C$ which is a representable morphism.

Contextual categories

Recall that if $C$ is a comprehension category, $\Gamma \in C$ is a “context” and $A\in E^{\Gamma }$ is a “type” in context $\Gamma$, we denote by $\Gamma .A$ the “extended context” in $C$.

Definition

A contextual category is a category with attributes $C$, def. 4, together with a length function $\ell :\mathrm{ob}(C)\to \mathbb{N}$ such that

1. There is a unique object of length $0$, which is a terminal object.
2. For any $\Gamma \in C$ and $A\in E^{\Gamma }$, we have $\ell (\Gamma .A)=\ell (\Gamma )+1$.
3. For any $\Delta \in C$ with $\ell (\Delta )>0$, there exists a unique $\Gamma \in C$ and $A\in E^{\Gamma }$ such that $\Delta =\Gamma .A$.

Remark

Since def. 6 refers to equality of objects, a contextual category $C$ must be a strict category.

Remark

The idea which distinguishes a contextual category is that “every context must be built out of types” in a unique way.

This makes for the closest match with type theory; in fact we have

Theorem

The category of contextual categories, def. 6, and (strictly) structure-preserving functors is equivalent to the category of dependent type theories and interpretations?.

Remark

Since contextual categories are strict categories, the category of such is really a 1-category, or perhaps a strict 2-category.

Definition

Given any category with attributes $C$, def. 4, possessing a terminal object, there is a canonical way to build a contextual category $\mathrm{cxt}(C)$, def. 6, from it.

1. Choose a terminal object $1\in C$ (the resulting contextual category does not depend on this choice, up to isomorphism).

2. The objects of $\mathrm{cxt}(C)$ are the finite lists

   $$(A_0,A_1,\dots ,A_n)$$(A_0,A_1,\dots,A_n)

   such that $A_0\in E^1$ and $A_{k+1}\in E^{1.A_0.A_1.\cdots .A_k}$ for all $k$.

3. The morphisms $(A_0,\dots ,A_n)\to (B_0,\dots ,B_m)$ in $\mathrm{cxt}(C)$ are the morphisms $1.A_0.A_1.\cdots .A_n\to 1.B_0.B_1.\cdots .B_m$ in $C$.

All the rest of the structure on $\mathrm{cxt}(C)$ is induced in an evident way from $C$.

Examples

Comprehension categories and display map categories are easy to come by “in nature”, but it is more difficult to find examples of the “split” versions of the above structure (which are what is needed for modeling type theory). Here we summarize some basic known constructions.

However, first we should mention the examples that come from type theory itself.

Syntactic categories

Example

The syntactic category of any dependent type theory has all of the above structures. Its objects are contexts in the theory, and the types in context $\Gamma$ form the set or category $E^{\Gamma }$. The strict associativity of substitution in type theory makes this fibration automatically split.

Splitting fibrations

There are standard constructions which can replace any Grothendieck fibration by an equivalent split fibration. Therefore,

Example

Given any comprehension category, def. 1,

1. we may replace it by a split comprehension category, def. 2,

2. then consider the underlying category with attributes, def. 4,

3. and finally pass to a contextual category by the construction in def. 7.

Of course, comprehension categories are easy to come by; perhaps they arise most commonly as display map categories. For instance, if $C$ has all pullbacks, then we can take all maps to be display maps. If $C$ is a category of fibrant objects, we can take the fibrations to be the display maps.

So, for the record, we have in particular:

Example

For $C$ a locally cartesian closed category $C$, it becomes a model for dependent type theory by regarding its codomain fibration $C^I\to C$ as a comprehension category, def. 1, and then strictifying that as in example 2.

Remark

It turns out that for modeling additional type-forming operations, however, not all splitting constructions are created equal.

Given $E\to C$, one classical construction (due to John Power) defines $E\prime \to C$, where an object of $E\prime$ over $\Gamma \in C$ consists of a morphism $f:\Gamma \to \Delta$ in $C$ along with an object $A$ of $E$ over $\Delta$. Type-theoretically, we can regard $(f,A)$ as a type $A$ with a “delayed substitution” $f$. This produces a split fibration (the chosen cartesian arrows are given by composition of morphisms in $C$), but it seems impossible to define dependent sums and products on it in a strict way.

A better choice is a construction due to Benabou, which defines the objects of $E\prime$ over $\Gamma \in C$ to be functors $C/\Gamma \to E$ over $C$ which map every morphism of $C/\Gamma$ to a cartesian arrow. Type-theoretically, we can think of such an object as a type together with specified compatible substitutions along any possible morphism. That type-formers can be extended in this case was proven by Martin Hofmann for dependent sums and dependent products and extensional identity types, and by Michael Warren in the case of intensional identity types (but not for the eliminator).

Universes

Suppose given a particular morphism $p:\tilde{U}\to U$ in $C$. We can then define a category with attributes, def. 4, as follows: the discrete fibration $E\to C$ corresponds to the representable presheaf $C(-,U)$, and the functor $E\to C^I$ is defined by pullback of $p$. We are thus treating $U$ as a “universe” of types. We can then of course pass to a contextual category, as described above.

Type-forming operations can be extended strictly in this case by performing them once in the “universal” case, then acting by composition. This construction is due to Voevodsky. It also meshes quite well with type theories that contain internal universes – a type of types– , and in particular for modeling the univalence axiom.

Particular important universes include:

• Any Grothendieck universe in Set, or more generally a universe in a topos. The resulting display maps are those with ”$U$-small fibers”.

• In the category Gpd, the groupoid of small groupoids. The resulting display maps are the split opfibrations with small fibers. Similarly, we can consider the groupoid of small sets, whose display maps are the discrete opfibrations with small fibers.

• In the category sSet of simplicial sets, there is a universal Kan fibration? $p:\tilde{U}\to U$ which classifies all Kan fibrations with small fibers.

Simple fibrations

Let $C$ be any category with finite products, and define $E\to C$ to be the discrete fibration corresponding to the presheaf $C^{\mathrm{op}}\to \mathrm{Set}$ which is constant at $\mathrm{ob}(C)$. Thus, the objects of $E$ are pairs $(\Gamma ,A)$ of objects of $C$, with the only morphisms being of the form $(\Gamma ,A)\to (\Delta ,A)$ induced by a morphism $\Gamma \to \Delta$ in $C$.

Define the functor $E\to C^I$ to take $(\Gamma ,A)$ to the projection $\Gamma \times A\to \Gamma$. It is straightforward to check that this defines a category with attributes. The corresponding (split) full comprehension category is called the simple fibration of $C$.

The dependent type theory which results from this structure “has no nontrivial dependency”. That is, whenever we have a dependent type $\Gamma ⊢(A\mathrm{type})$, it is already the case that $A$ is a type in the empty context (that is, we have $⊢(A\mathrm{type})$), and so it cannot depend nontrivially on $\Gamma$. In effect, it is not really a dependent type theory, but a simple (non-dependent) type theory — hence the name “simple fibration”.

Related pages

• categorical semantics

• relation between type theory and category theory

References

A general overview can be found in

• Martin Hofmann, Syntax and semantics of dependent types, Semantics and logics of computation (Cambridge, 1995), Publ. Newton Inst., vol. 14, Cambridge Univ. Press, Cambridge, 1997, pp. 79–130

Comprehension categories are defined in

• Bart Jacobs, Comprehension categories and the semantics of type dependency, Theoret. Comput. Sci. 107 (1993), no. 2, 169–207

Display maps are discussed in

• Paul Taylor, Practical Foundations of Mathematics, section 8.3

Categories with attributes are discussed in

• John Cartmell, Generalised algebraic theories and contextual categories, Ph.D. thesis, Oxford, 1978

• Eugenio Moggi, A category-theoretic account of program modules, Math. Structures Comput. Sci. 1 (1991), no. 1, 103–139

• Andrew M. Pitts, Categorical logic, Handbook of logic in computer science, Vol. 5, Handb. Log. Comput. Sci., vol. 5, Oxford Univ. Press, New York, 2000, pp. 39–128

Categories with families are defined in

• Peter Dybjer, Internal type theory, Types for proofs and programs (Torino, 1995), Lecture Notes in Comput. Sci., vol. 1158, Springer, Berlin, 1996, pp. 120–134, PDF

and shown to be equivalent to categories with attributes in

• Martin Hofmann, Syntax and semantics of dependent types, citeseer.

Contextual categories are defined in

• John Cartmell, Generalised algebraic theories and contextual categories, Ann. Pure Appl. Logic 32 (1986), no. 3, 209–243

• Thomas Streicher, Semantics of type theory, Progress in Theoretical Computer Science, Birkhäuser Boston Inc., Boston, MA, 1991, Correctness, completeness and independence results.

Strictification is discussed in

• Martin Hofmann, On the interpretation of type theory in locally cartesian closed categories

• Vladimir Voevodsky, Notes on type systems