nLab categorical semantics of dependent type theory

Idea

In the relation between type theory and category theory, dependent types (in dependent type theory) have categorical semantics given by morphisms which are the bundles whose fibers are the families indexed by the base (see also at dependent type – Relation to families of elements).

More concretely: if a type $A$ interprets as an object in some category $\mathcal{C}$, then an $A$-dependent type

$$(x \colon A) \;\;\;\vdash\;\;\; B(x) \;Type$$

interprets as a morphism $B \to A$ in $\mathcal{C}$ (hence as an object in the slice category $\mathcal{C}_{/A}$). We may think of this morphism as a bundle or fibration, whose fiber over $x \colon 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 (but see at substitution – Categorical semantics for more); that is, given a term

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

corresponding to a morphism $f:C\to A$, the substituted dependent 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:D) \;\vdash\; (B(f(g(z))) \;type)$$

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

One of these structures is called “contextual categories” (definition 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 corresponds 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)

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 strictly commutative triangle of functors

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

where $C^I$ is the arrow category of $C$ and $cod \colon C^I \to C$ denotes the codomain projection (which is a fibration if $C$ has pullbacks), and such that

1. $E\to C$ is a Grothendieck fibration,

2. $E\to C^I$ takes cartesian morphisms in $E$ to cartesian morphisms in $C^I$ (i.e. to pullback squares in $C$).

Remark

In def 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 (def. ) is called

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

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

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 def. 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 (def. ), 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 themselves 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 (def. ). Thus, we have:

Lemma

Display map categories (def. ) may be identified with those comprehension categories, def. , 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. , (those where $E\to C^I$ is merely fully faithful).

However, this breaks down when we are interested in split comprehension categories, def. , 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. , for which $E\to C$ is a discrete fibration.

Remark

That is, in a category with attributes (def. ) 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. , 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 functor. In this way, we obtain:

Lemma

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

(These are, however, quite different as subcategories of $\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,B\in E^\Gamma$, then we may think of a morphism $f:A\to B$ in $E^\Gamma$ as a term

(1)$$(\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)$$(\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 $Fam$ denote the category of families of sets. Its objects 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\colon I\to J$ and functions $g_i \colon A_i \to B_{f(i)}$. We can equivalently, of course, regard this as the arrow category $Set^I$ of Set, where $(B_j)_{j\in J}$ corresponds to the arrow $\coprod B \to J$.

Definition

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

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

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

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

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

We can then prove:

Lemma

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

Proof

Given a category with families, let $E\to C$ be the Grothendieck construction of the functor $Ty:C^{op}\to Set$, and let $E\to C^I$ take each $A\in Ty(\Gamma)$ to the above representing object. This is a category with attributes.

Conversely, given a category with attributes, let $Ty:C^{op}\to Set$ be the functor corresponding to the discrete fibration $E\to C$, and for $A\in Ty(\Gamma)$ let $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.

Natural Models

Awodey 2016 presented the following “natural model” of type theory as an alternative to categories with families.

Theorem

If we modify Def. by requiring only that the functors $(\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 $C$, together with
2. a morphism $Tm \to Ty$ in the category of presheaves on $C$ which is a representable morphism.

The category $C$ models the category of contexts and substitutions, and the morphism $Tm \to Ty$ models the bundle of (context-dependent) terms over (context-dependent) types. The representability models the extension of a context with a new typed variable.

The condition that $Tm \to Ty$ is a representable morphism in presheaves can be reformulated in terms of adjoints as follows: $Tm \to Ty$ is representable just if the associated functor ${\int Tm} \to {\int Ty}$ has a right adjoint. Thus a natural model can be equivalently described as a category $C$ equipped with a natural transformation of presheaves $Tm \to Ty$ for which ${\int Tm} \to {\int Ty}$ has a right adjoint.

This specification can be related to that of a , by reformulating the representability of the morphism $Tm \to Ty$ in terms of representable profunctors as follows. A natural model is equivalently described as:

1. a category $C$,
2. a presheaf $Ty : \hat C$ of types in context.
3. a presheaf $Tm : \widehat {\int Ty}$ of typed terms in context.
4. a functor $ext : \widehat {\int Ty} \to C$ of context extension with data that represents the profunctor ${\int Ty}(ty-,=) \odot C(-,ctx(ty(=))) : \int Ty ⇸ C$ where $ty : \int Tm \to \int Ty$ and $ctx : \int Ty \to C$ are the projections of the Grothendieck construction.

Writing the profunctor as P, it is equivalent to the following definition:

$$P(\Delta, (\Gamma, A)) = (\gamma : \Delta \to \Gamma) \times (a : Tm(\Delta, A[\gamma]))$$

then the universal property of the context extension is that there is a natural isomorphism $\Delta \to ext(\Gamma, A) \cong P(\Delta,(\Gamma,A))$

Categories with Representable Maps

Taichi Uemura introduced categories with representable maps? as a functorial semantics approach to type theory generalizing the notion of a Category with Families/Natural Model. A category with representable maps (CwR) is a category with finite limits with a specified class of “representable” arrows that are pullback-stable and exponentiable. The motivating examples are presheaf categories where the representable arrows are the representable morphisms in the usual sense. Then any CwR can be considered to be a type theory: for instance, the free CwR with a representable map $Tm \to Ty$ has as models precisely the natural models, and so can be thought of as the embodiment of the judgments of Martin-Lof Type Theory (with no connectives).

Contextual categories, or C-systems

Recall that

Definition

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

Definition

A contextual category (Cartmell 86, Streicher 91) or C-system (Voevodsky 15) is a category with attributes $C$ (def. ) together with a length function $\ell : 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)\gt 0$, there exists a unique $\Gamma\in C$ and $A\in E^\Gamma$ such that $\Delta = \Gamma.A$ (with notation as in def. ).

Remark

Since def. 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. , 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.

Example

Given any category with attributes $C$, def. , possessing a terminal object, there is a canonical way to build a contextual category $cxt(C)$, def. , 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 $cxt(C)$ are the finite lists

   $$(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 $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 $cxt(C)$ is induced in an evident way from $C$. This construction is in fact right adjoint to the inclusion of contextual categories in categories with attributes; see Kapulkin-Lumsdaine, Proposition 4.4.

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. we may replace it by a split comprehension category, def. ,

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

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

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. , and then strictifying that as in example .

Remark

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

Given $E\to C$, one construction due to Benabou (called the “right adjoint splitting”), defines $E'\to C$, where the objects of $E'$ over $\Gamma\in C$ are 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 may be extended in this case was proven by Martin Hofmann for dependent sums and dependent products and the identity types of extensional type theory. But this is not generally possible for the identity types of intensional type theory (particularly not their eliminator), which do not have a 1-categorical universal property and hence are not stable under pullback up to isomorphism.

A different construction (due to John Power, called the “left adjoint splitting”) defines an object of $E'$ over $\Gamma\in C$ to consist 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$), and it was proven by Lumsdaine & Warren (2015) that essentially all type formers can be extended to it from $E$.

Universes

Suppose given a particular morphism $p:\widetilde{U} \to U$ in $C$. We can then define a category with attributes, def. , 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 may then of course pass to a contextual category, via example .

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:

• 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:\widetilde{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^{op}\to Set$ which is constant at $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 \vdash (A \;type)$, it is already the case that $A$ is a type in the empty context (that is, we have $\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”.

The big model of locally cartesian closed categories

Example

Ignoring coherence issues, the CwF induced by a locally cartesian closed (lcc) category $\mathcal{C}$ (example ) is given explicitly by the “Explicit” column of the following table:

	In $\mathcal{C}$: Explicit	In terms of slices of $\mathcal{C}$	Big model
Contexts	Objects $\Gamma \in \mathcal{C}$	Slice categories $\mathcal{C}_{/ \Gamma}$	Lcc categories $\Gamma$
Context Morphisms	Morphisms $f : \Gamma \rightarrow \Delta$	Lcc functors $f^* : \mathcal{C}_{/ \Delta} \rightarrow \mathcal{C}_{/ \Gamma}$ over $\mathcal{C}$	Lcc functors $f : \Delta \rightarrow \Gamma$
Types	Morphisms $\sigma : \operatorname{dom} \sigma \rightarrow \Gamma$	Objects $\sigma \in \mathcal{C}_{/ \Gamma}$	Objects $\sigma \in \Gamma$
Terms	Sections $s : \Gamma \leftrightarrows \operatorname{dom} \sigma : \sigma$	Morphisms $s : \mathrm{id}_\Gamma \rightarrow \sigma$ in $\mathcal{C}_{/ \Gamma}$	Morphisms $s : 1 \rightarrow \sigma$ in $\Gamma$, where $1$ is a terminal object.
Substitution	Pullback along $f$	Application of $f^*$	Application of $f$

The next column describes the same CwF in the terminology of slice categories: Every object of $\mathcal{C}$ corresponds to a slice category $\mathcal{C}_{/ \Gamma}$ over $\mathcal{C}$, and $\mathcal{C}_{/ \Gamma}$ is also lcc. Every morphism $f : \Gamma \rightarrow \Delta$ in $\mathcal{C}$ induces a pullback functor $f^* : \mathcal{C}_{/ \Delta} \rightarrow \mathcal{C}_{/ \Gamma}$. $f^*$ preserves the finite limits and dependent products of $\mathcal{C}_{/ \Delta}$ (i.e. it is an lcc functor), and the diagram

$$\array{ && \mathcal{C} \\ & {}_{\Delta^*} \swarrow && \searrow_{\Gamma^*} \\ \mathcal{C}_{/ \Delta} && \stackrel{\to}{f^*} && \mathcal{C}_{/ \Gamma} }$$

commutes (up to unique isomorphism). Conversely, every lcc functor $\mathcal{C}_{/ \Delta} \rightarrow \mathcal{C}_{/ \Gamma}$ under $\mathcal{C}$ is uniquely isomorphic to the pullback functor along some morphism $\Gamma \rightarrow \Delta$.

The last column describes the big model of type theory in the opposite category of lcc categories and lcc functors. Since the contexts of this model are itself models of type theory, it can be understood as a “model of models”. The definition of the big model can be arrived at by removing all reference to the fixed lcc category $\mathcal{C}$ in the previous column. Instead of just the slice categories of $\mathcal{C}$, now all lcc categories are allowed as contexts. Context morphisms are generalized to general lcc functors instead of just the pullback functors of $\mathcal{C}$. The identity morphism on an object $\Gamma$ of $\mathcal{C}$ is a terminal object in the slice category $\mathcal{C}_{/ \Gamma}$ and is thus generalized to a terminal object in any lcc category.

The usual model in a fixed lcc category $\mathcal{C}$ can be recovered from the big model by slicing: The contextual core (example ) of the slice of the big model over $\mathcal{C}$ is equivalent to $\mathcal{C}$.

However, the naive definition of the big model above suffers from the same coherence issues as the standard models in individual lcc categories: Lcc functors preserve lcc structure (i.e. type formers) up to isomorphism, but not necessarily up to equality. These coherence problems can be resolved by working with a suitable model categorical presentation of the $(2, 1)$-category of lcc categories, lcc functors and natural isomorphisms. Note that the model category presenting a higher category is unique up to zig-zag of Quillen equivalences, but that the underlying 1-categories of these model categories can vary non-trivially. Because coherence issues are ultimately about equations in the underlying 1-category, we can thus hope that some model categories presenting the category of lcc categories will be better behaved than others for our purpose.

One possible way to construct such a well-behaved model category is as follows (see (Bidlingmaier 2020) for details):

1. First one defines a model category $\mathrm{Lcc}$ of lcc sketches. An lcc sketch is a category with some diagrams marked as finite limits cones and evalution maps of dependent products. These marked diagrams do not need to satisfy the corresponding universal property, however. The model category structure is set up such that every object is cofibrant, and the fibrant objects are precisely the lcc categories with diagrams marked if and only if they satisfy the corresponding universal property. Thus the subcategory of fibrant objects of $\mathrm{Lcc}$ corresponds to the usual category of lcc categories. Note however, that lcc categories in the sense of fibrant lcc sketches “have” finite limits and dependent products in the sense that these universal objects merely exist; there are no distinguished/assigned choices of universal objects. Thus preservation of universal objects by functors up to equality (i.e. strictness of substitution) cannot even be stated in $\mathrm{Lcc}$.

2. The model category $\mathrm{sLcc}$ of strict lcc categories is defined as the category of algebraically fibrant objects of $\mathrm{Lcc}$; it is Quillen equivalent to $\mathrm{Lcc}$. Assigned lifts against the trivial cofibrations of $\mathrm{Lcc}$ correspond to distinguished choices of universal objects, and these choices are preserved by the morphisms of $\mathrm{sLcc}$, the strict lcc functors. Thus $\mathrm{sLcc}$ supports substitutions that preserve type formers up to equality.

   However, it does not support some dependent type formers in any obvious way, notably not $\Sigma$ and $\Pi$ types. The problem is that the context extension $\Gamma.\sigma$ of some $\Gamma \in \operatorname{Ob} \mathrm{sLcc}$ by a type (i.e. object) $\sigma$ of $\Gamma$ is given by freely (in the 1-categorical sense) adjoining a morphism $1 \rightarrow \sigma$ to $\Gamma$. To interpret $\Sigma$ and $\Pi$ types, one has to relate $\Gamma.\sigma$ with the slice category $\Gamma_{/ \sigma}$ in some way, and it appears that this is not generally possible. Note that $\Gamma_{/ \sigma}$ has the universal property of a context extension in the higher/bicategorical sense, but that $\Gamma.\sigma$ is defined purely 1-categorically.

3. To reconcile context extensions $\Gamma.\sigma$ with slice categories $\Gamma_{/ \sigma}$, one can work with the algebraically cofibrant objects of $\mathrm{sLcc}$. An algebraically cofibrant object of $\mathrm{sLcc}$ is a coalgebra for a fixed cofibrant replacement comonad. The category of such coalgebras has model category structure, and this model category is again Quillen equivalent to $\mathrm{sLcc}$.

   A cofibrant object $\Gamma$ of $\mathrm{sLcc}$ has the property that every non-strict lcc functor (i.e. morphism of underlying lcc sketches) out of $\Gamma$ is isomorphic to a strict lcc functor. This property turns out to be sufficient to construct a weak equivalence $\Gamma.\sigma \rightarrow \Gamma_{/ \sigma}$ in $\mathrm{sLcc}$. For algebraically cofibrant $\Gamma$, this weak equivalence is structure and hence preserved by coalgebra morphisms up to equality. This turns out to be sufficient to endow the category of algebraically cofibrant objects of $\mathrm{sLcc}$ with CwF structure that supports finite limit, $\Sigma$ and $\Pi$ type constructors.

Related pages

• fibration category

  • clan, tribe

  • type-theoretic model category

• categorical semantics

• relation between type theory and category theory

• initiality conjecture

• Awodey's conjecture

• model of type theory in an (infinity,1)-topos

References

The general idea of categorical semantics of dependent types goes back at least to Seely 1984, a first formalization via categories with display maps (“clans”) is due to:

• Paul Taylor, §4.3.2 in: Recursive Domains, Indexed Category Theory and Polymorphism, Cambridge (1983-7) [pdf]

• Paul Taylor, Section 8.3 in: Practical Foundations of Mathematics, Cambridge University Press (1999) [webpage]

General overview:

• 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]

which originates as

• Martin Hofmann, chapter 2 of: 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]

Texbook accounts:

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

Comprehension categories are defined in

• Bart Jacobs, Comprehension categories and the semantics of type dependency, Theoret. Comput. Sci. 107 2 (1993) 169-207 [MR1201808, doi:10.1016/0304-3975(93)90169-T]

A 2-categorical treatment of variant kinds of comprehension category is given in

• Paul-André Melliès, Nicolas Rolland, Comprehension and quotient structures in the language of 2-categories, (arXiv:2005.10015)

A correspondence with orthogonal factorization systems is discussed in

• Clemens Berger, Ralph M. Kaufmann, Comprehensive factorisation systems (pdf)

Categories with attributes are discussed in

• John Cartmell, Generalised algebraic theories and contextual categories, Ph.D. thesis, Oxford (1978), Ann. Pure Appl. Logic 32 3 (1986) 209–243 [doi:10.1016/0168-0072(86)90053-9MR865990]

• Eugenio Moggi, A category-theoretic account of program modules, Math. Structures Comput. Sci. 1 1 (1991) 103-139 [MR1108806, doi:10.1017/S0960129500000074]

• Andrew M. Pitts, Categorical logic, in Handbook of Logic in Computer Science 5 Oxford Univ. Press (2000) 39-128 [doi:10.1093/oso/9780198537816.003.0002, pdf, MR1859470]

Categories with families are defined in

• Peter Dybjer, Internal type theory, Types for proofs and programs (Torino, 1995), Lecture Notes in Comput. Sci. 1158 Springer (1996) 120-134 [doi:10.1007/3-540-61780-9_66, pdf, MR1474535]

and shown to be equivalent to categories with attributes in Hofmann (1997)

The formulation in terms of representable natural transformations (natural models of homotopy type theory) is due to:

• Steve Awodey, Natural models of homotopy type theory, Mathematical Structures in Computer Science, 28 2 (2016) 241-286 [arXiv:1406.3219, doi:10.1017/S0960129516000268]

See also

• Clive Newstead, Algebraic models of dependent type theory [arXiv:2103.06155]

A proof of initiality for dependent type theory is claimed in

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

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

• Thorsten Altenkirch, Ambrus Kaposi, Type Theory in Type Theory using Quotient Inductive Types, (2015) (pdf), (formalisation in Agda).

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 – Correctness, completeness and independence results, Progress in Theoretical Computer Science, Birkhäuser (1991) [ISBN:0-8176-3594-7, doi:10.1007/978-1-4612-0433-6, MR1134134]

Review:

• Chris Kapulkin, Peter LeFanu Lumsdaine, section 1.2 and appendix B of The Simplicial Model of Univalent Foundations (after Voevodsky) (arXiv:1211.2851)

Contextual categories as models for homotopy type theory are discussed in

• Chris Kapulkin, Peter LeFanu Lumsdaine, The homotopy theory of type theories, Advances in Mathematics 337 (2018) 1-38 [arXiv:1610.00037, doi:10.1016/j.aim.2018.08.003]

• André Joyal, Notes on Clans and Tribes [arXiv:1710.10238]

Further discussion of contextual categories is in

• Vladimir Voevodsky, A C-system defined by a universe category, Theory Appl. Categ. 30 (2015), No. 37, 1181–1215, arXiv:1409.7925 (arXiv:1409.7925)

• Vladimir Voevodsky, Martin-Löf identity types in the C-systems defined by a universe category (arXiv:1505.06446)

• Vladimir Voevodsky, Products of families of types in the C-systems defined by a universe category (arXiv:1503.07072)

• Vladimir Voevodsky, Subsystems and regular quotients of C-systems (arXiv:1406.7413)

Discussion of B-systems, another essentially algebraic model, is in

• Vladimir Voevodsky, B-systems (arXiv:1410.5389)

The model of dependent type theory with dependent product types/dependent function types in locally cartesian closed categories was first made explicit in

• R. A. G. Seely, Locally cartesian closed categories and type theory, Math. Proc. Camb. Phil. Soc. 95 (1984) 33-48 [doi:10.1017/S0305004100061284, pdf]

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 (1993) 51-86 [doi:10.5555/175469.175471] and: Diagrammes 23 (1990) 43-66 [numdam:DIA_1990__23__43_0]

• Martin Hofmann, On the interpretation of type theory in locally cartesian closed categories, in Computer Science Logic. CSL 1994, Lecture Notes in Computer Science 933 (1994) 427–441 [doi:10.1007/BFb0022273]

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, in Typed lambda calculi and applications, Lecture Notes in Comput. Sci. 6690 Springer (2011) [arXiv:1112.3456, doi:10.1007/978-3-642-21691-6_10]

and

• Pierre-Louis Curien, Richard Garner, Martin Hofmann, Revisiting the categorical interpretation of dependent type theory, Theoretical Computer Science 546 21 (2014) 99-119 [doi:10.1016/j.tcs.2014.03.003, pdf]

See also:

• Peter LeFanu Lumsdaine, Michael Warren, The local universes model: An overlooked coherence construction for dependent type theory, ACM Trans. Comput. Log., 16 3 no 23 (2015) 1-31 [arXiv:1411.1736, doi:10.1145/2754931]

• Vladimir Voevodsky, Notes on type systems

Comparisons of various models can be found in

• Benedikt Ahrens, Peter LeFanu Lumsdaine, Vladimir Voevodsky, Categorical structures for type theory in univalent foundations [arxiv:1705.04310]

• Chris Kapulkin, Peter LeFanu Lumsdaine, The homotopy theory of type theories[arXiv:1610.00037]

• Daniel Gratzer, Jonathan Sterling, Syntactic categories for dependent type theory: sketching and adequacy [arXiv:2012.10783]

Recent work on abstract definitions of (models of) type theory include:

• Valery Isaev, Algebraic Presentations of Dependent Type Theories (arXiv:1602.08504)

• Taichi Uemura, A General Framework for the Semantics of Type Theory (arXiv:1904.04097)

A category with families structure is constructed on the $(2,1)$-category of all locally cartesian closed categories, which since locally presentable may be treated via model categories, in:

• Martin Bidlingmaier, An interpretation of dependent type theory in a model category of locally cartesian closed categories, (arXiv:2007.02900)

• Michael Ching, Emily Riehl, Coalgebraic models for combinatorial model categories arXiv:1403.5303

• Valery Isaev, Model category of marked objects arXiv:1610.08459

An equivalence between contextual categories and B-systems is in:

• Benedikt Ahrens, Jacopo Emmenegger, Paige Randall North, Egbert Rijke, Algebraic Presentations of Dependent Type Theories (arXiv:2111.09948)