categorical model of dependent types


Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism = propositions as types +programs as proofs +relation type theory/category theory

logiccategory theorytype theory
trueterminal object/(-2)-truncated objecth-level 0-type/unit type
falseinitial objectempty type
proposition(-1)-truncated objecth-proposition, mere proposition
proofgeneralized elementprogram
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
cut elimination for implicationcounit for hom-tensor adjunctionbeta reduction
introduction rule for implicationunit for hom-tensor adjunctioneta conversion
logical conjunctionproductproduct type
disjunctioncoproduct ((-1)-truncation of)sum type (bracket type of)
implicationinternal homfunction type
negationinternal hom into initial objectfunction type into empty type
universal quantificationdependent productdependent product type
existential quantificationdependent sum ((-1)-truncation of)dependent sum type (bracket type of)
equivalencepath space objectidentity type
equivalence classquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
completely presented setdiscrete object/0-truncated objecth-level 2-type/preset/h-set
setinternal 0-groupoidBishop set/setoid
universeobject classifiertype of types
modalityclosure operator, (idemponent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels


Category theory

Categorical models of dependent types


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 AA corresponds to an object in some category, then a dependent type

(x:A)(B(x)type) (x:A) \;\vdash\; (B(x) \;type)

corresponds to a morphism BAB\to A in that category. We think of this morphism as a bundle or fibration, whose fiber over x:Ax:A is the type B(x)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 (but see at substitution – Categorical semantics for more); that is, given a term

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

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

(y:C)(B(f(y))type) (y:C) \;\vdash\; (B(f(y)) \;type)

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

(z:D)(B(f(g(z)))type) (z:D) \;\vdash\; (B(f(g(z))) \;type)

is syntactically the same regardless of whether we obtain it by substituting yg(z)y \coloneqq g(z) into B(f(y))B(f(y)), or xf(g(z))x \coloneqq f(g(z)) into B(x)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.

One of these structures is called “contextual categories” (definition 7 below). This and other kinds of categories-with-extra-structure may hence be thought of as stand-ins for the syntax of a type theory:

Rather than constructing an interpretation of the syntax directly, we may work via the intermediary notion of contextual categories, a class of algebraic objects abstracting the key structure carried by the syntax. The plain definition of a contextual category coresponds to the structural core of the syntax; further syntactic rules (logical constructors, etc.) correspond to extra algebraic structure that contextual categories may carry. Essentially, contextual categories provide a completely equivalent alternative to the syntactic presentation of type theory.

Why is this duplication of notions desirable? The trouble with the syntax is that it is mathematically tricky to handle. Any full presentation must account for (among other things) variable binding, capture-free substitution, and the possibility of multiple derivations of a judgement; and so a direct interpretation must deal with all of these, at the same time as tackling the details of the particular model in question. By passing to contextual categories, one deals with these subtleties and bureaucracy once and for all, and obtains a clear framework for subsequently constructing models. Conversely, why not work only with contextual categories, dispensing with syntax entirely?

The trouble on this side is that working with higher-order logical structure in contextual categories quickly becomes unreadable. The reader preferring to take contextual categories as primary may regard the syntax as essentially a notation for working within them: a powerful, flexible, and intuitive notation, but one whose validity requires non-trivial work to establish. (The situation is comparable to that of string diagrams, as used in monoidal and more elaborately structured categories.

(from Kapulkin-Lumsdaine 12)


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

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

Sometimes, we want to consider CC 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 CC 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


A comprehension category consists of a strictly commutative triangle of functors

E C I cod C \array{ E && \to && C^I\\ & \searrow && \swarrow {\scriptsize cod} \\ && C }

where C IC^I is the arrow category of CC and cod:C ICcod \colon C^I \to C denotes the codomain fibration, and such that

  1. ECE\to C is a Grothendieck fibration,

  2. EC IE\to C^I takes cartesian morphisms in EE to cartesian morphisms in C IC^I (i.e. to pullback squares in CC).


In def 1 we do not ask that C ICC^I \to C be a fibration (that would require CC to have all pullbacks), only that the particular morphisms in the image of EE are cartesian.


A comprehension category (def. 1) is called

In the latter case, we must consider EE 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.


The interpretation of def. 1 is as follows:

In a comprehension category, we may regard the objects of CC as contexts, and the fiber E ΓE^\Gamma of ECE\to C over an object Γ\Gamma as the category of dependent types in context Γ\Gamma. If the comprehension category is split (def. 2), then such dependent types have strictly associative substitution.

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

Display map categories


A display map category consists of a category CC together with a class DD of morphisms in CC, called display maps, such that all pullbacks of display maps exist and are themselves display maps.

If CC is a display map category, then by defining EE to be the full subcategory of C IC^I whose objects are display maps, we obtain a full comprehension category (def. 2). Thus, we have:


Display map categories (def. 3) may be identified with those comprehension categories, def. 1, for which the functor EC IE\to C^I is the inclusion of a full subcategory.


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 EC IE\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 EE 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


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


That is, in a category with attributes (def. 4) 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 CC 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 EC IE\to C^I be fully faithful.

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


The category CwA\mathbf{CwA} of categories with attributes (def. 4) is equivalent to the category of CompCat full,split\mathbf{CompCat}_{\text{full,split}} of full split comprehension categories (def. 2).

(These are, however, quite different as subcategories of CompCat\mathbf{CompCat}.)

Categories with families

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

(1)(x:Γ),(a:A(x))(f(x,a):B(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)(x:Γ)(f(x):B(x)) (\vec{x} : \Gamma) \;\vdash\; (f(\vec{x}) : B(\vec{x}))

in type theory.


A term of the form (1) can equivalently be regarded as a term of the form (2) by replacing Γ\Gamma by the extended context Γ.A\Gamma.A, and BB by its substitution along the projection Γ.AΓ\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 CC, as in a category with attributes or a full comprehension category, then instead of specifying the functor EC IE\to C^I and then asking either that it be fully faithful or that EE be discrete (removing the information about extra morphisms in EE), if we specify the terms of the form (2), then the functor EC IE\to C^I is determined by a universal property.

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


A category with families is a category CC together with

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

  • For each ΓC\Gamma\in C and ATy(Γ)A\in Ty(\Gamma), a representing object for the functor

    (C/Γ) op Set (ΔfΓ) Tm(f *(A)) \begin{aligned} (C/\Gamma)^{op} & \to Set\\ (\Delta \xrightarrow{f} \Gamma) & \mapsto Tm(f^*(A)) \end{aligned}

Intuitively, F(Γ)F(\Gamma) is the set of terms in the context Γ\Gamma indexed by their type, and the representing object for the map (C/Γ) opSet(C/\Gamma)^{op} \to Set is the context Γ;A\Gamma; A.

We can then prove:


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


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

The following alternative characterization was observed by Steve Awodey.


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

  1. a category CC, together with
  2. a morphism TmTyTm \to Ty in the category of presheaves on CC which is a representable morphism.

Contextual categories, or C-systems

Recall that


If CC is a comprehension category (def. 1), ΓC\Gamma\in C is a “context” and AE ΓA\in E^\Gamma is a “type” in context Γ\Gamma, then we denote by Γ.A\Gamma.A the “extended context” in CC (remark 2).


A contextual category (Cartmell 86, Streicher 91) or C-system (Voevodsky 15) is a category with attributes CC (def. 4) together with a length function :ob(C)\ell : ob(C) \to \mathbb{N} such that

  1. There is a unique object of length 00, which is a terminal object.
  2. For any ΓC\Gamma\in C and AE ΓA\in E^\Gamma, we have (Γ.A)=(Γ)+1\ell(\Gamma.A) = \ell(\Gamma)+1.
  3. For any ΔC\Delta\in C with (Δ)>0\ell(\Delta)\gt 0, there exists a unique ΓC\Gamma\in C and AE ΓA\in E^\Gamma such that Δ=Γ.A\Delta = \Gamma.A (with notation as in def. 6).

Since def. 7 refers to equality of objects, a contextual category CC must be a strict category.


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:


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


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


Given any category with attributes CC, def. 4, possessing a terminal object, there is a canonical way to build a contextual category cxt(C)cxt(C), def. 7, from it.

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

  2. The objects of cxt(C)cxt(C) are the finite lists

    (A 0,A 1,,A n)(A_0,A_1,\dots,A_n)

    such that A 0E 1A_0 \in E^1 and A k+1E 1.A 0.A 1..A kA_{k+1} \in E^{1.A_0.A_1.\cdots .A_k} for all kk.

  3. The morphisms (A 0,,A n)(B 0,,B m)(A_0,\dots,A_n) \to (B_0,\dots,B_m) in cxt(C)cxt(C) are the morphisms 1.A 0.A 1..A n1.B 0.B 1..B m1.A_0.A_1.\cdots.A_n \to 1.B_0.B_1.\cdots.B_m in CC.

All the rest of the structure on cxt(C)cxt(C) is induced in an evident way from CC.


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


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 Γ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,


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 example 1.

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

So, for the record, we have in particular:


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


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

Given ECE\to C, one classical construction (due to John Power) defines ECE'\to C, where an object of EE' over ΓC\Gamma\in C consists of a morphism f:ΓΔf:\Gamma \to \Delta in CC along with an object AA of EE over Δ\Delta. Type-theoretically, we can regard (f,A)(f,A) as a type AA with a “delayed substitution” ff. This produces a split fibration (the chosen cartesian arrows are given by composition of morphisms in CC), 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 EE' over ΓC\Gamma\in C to be functors C/ΓEC/\Gamma \to E over CC which map every morphism of C/Γ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 may 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).


Suppose given a particular morphism p:U˜Up:\widetilde{U} \to U in CC. We can then define a category with attributes, def. 4, as follows: the discrete fibration ECE\to C corresponds to the representable presheaf C(,U)C(-,U), and the functor EC IE\to C^I is defined by pullback of pp. We are thus treating UU as a “universe” of types. We may then of course pass to a contextual category, via example 3.

Type-forming operations may 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:

Simple fibrations

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

Define the functor EC IE\to C^I to take (Γ,A)(\Gamma,A) to the projection Γ×AΓ\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 CC.

The dependent type theory which results from this structure “has no nontrivial dependency”. That is, whenever we have a dependent type Γ(Atype)\Gamma \vdash (A \;type), it is already the case that AA is a type in the empty context (that is, we have (Atype)\vdash (A\; 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”.


A general overview may 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

Categories with attributes are discussed in

  • John Cartmell, Generalised algebraic theories and contextual categories, Ph.D. thesis, Oxford, 1978 (GitHub LaTeXing project, organised by Peter LeFanu Lumsdaine. Currently only sections 1.0-1.4 are done)

  • 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

The initial category with families was constructed in

  • Simon Castellan, Dependent type theory as the initial category with families (PDF)

This was formalized inside type theory with set quotients of higher inductive types in:

Contextual categories were defined in

  • John Cartmell, Generalised algebraic theories and contextual categories, Annals of Pure and Applied Logic Volume 32, 1986, Pages 209-243 (doi:10.1016/0168-0072(86)90053-9)

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

Review includes

Contextual categories as models for homotopy type theory are discussed in

Further discussion of contextual categories is in

Strictification is discussed in

Revised on January 12, 2017 13:50:06 by Urs Schreiber (