The semantics of type theory involves several closely related kinds of models, which are constructed and studied in order to justify axioms and new type theories, and to use type theory as an internal language for categories, higher categories and other mathematical structures.

There are several ways to package the structure of a model of type theory, including categories with families, comprehension categories, categories with attributes and contextual categories.^[1] In all cases, a model is a base substrate, together with extra structure and requirements for each rule of the type theory under consideration.

Categories with families, introduced by Dybjer,^[2] are a commonly used notion of model which stays relatively close to the syntax of type theory.

The CwF structure is designed to closely parallel the syntax of type theory.

• To each derivable syntactic judgment of the form “${\displaystyle \Gamma }$ is a context”, the semantics in a CwF associates an element ${\displaystyle {\hat {\Gamma }}}$ of a set of contexts denoted ${\displaystyle \operatorname {Con} }$.
• To each derivable judgment “${\displaystyle A}$ is a type in context ${\displaystyle \Gamma }$” is associated an element ${\displaystyle {\hat {A}}}$ of a set of types in context ${\displaystyle {\hat {\Gamma }}}$ denoted ${\displaystyle \operatorname {Ty} ({\hat {\Gamma }})}$. (Here ${\displaystyle {\hat {A}}}$ depends on ${\displaystyle \Gamma }$ and not merely on ${\displaystyle A}$ although this dependency is dropped in the notation.)
• To each derivable judgment “${\displaystyle t}$ is a term of type ${\displaystyle A}$ in context ${\displaystyle \Gamma }$” (usually denoted ${\displaystyle \Gamma \vdash t:A}$) is associated an element ${\displaystyle {\hat {t}}}$ of a set of terms of type ${\displaystyle {\hat {A}}}$ in context ${\displaystyle {\hat {\Gamma }}}$, denoted ${\displaystyle \operatorname {Tm} _{\hat {\Gamma }}({\hat {A}})}$.

The semantic interpretation of definitional equality is always actual equality in the model, so whenever a judgment “${\displaystyle A}$ and ${\displaystyle B}$ are definitionally equal types in context ${\displaystyle \Gamma }$” is derivable, the interpretation in the model must ensure ${\displaystyle {\hat {A}}={\hat {B}}}$, and whenever “${\displaystyle t}$ and ${\displaystyle u}$ are definitionally equal terms of type ${\displaystyle A}$ in context ${\displaystyle \Gamma }$” is derivable, the interpretation ensures ${\displaystyle {\hat {t}}={\hat {u}}}$.

A CwF contains operations to interpret contexts: a special element ${\displaystyle \diamond \in \operatorname {Con} }$ to model the empty context, and a context extension operation ${\displaystyle \triangleright }$ to model the addition of a new variable to a context.

The remaining data of CwFs serves to interpret the substitution operation necessitated by dependent types: if ${\displaystyle f}$ has the dependent function type ${\displaystyle (x:A)\to B}$ where ${\displaystyle B}$ is a term involving the variable ${\displaystyle x}$, the application of ${\displaystyle f}$ to a term ${\displaystyle t}$ has the type ${\displaystyle B[x:=t]}$. CwFs use parallel substitutions, namely substitutions between entire contexts. If there were a judgment in the syntax which was directly interpreted by a substitution from ${\displaystyle {\hat {\Gamma }}}$ to ${\displaystyle {\hat {\Delta }}}$ in the CwF, it would be “${\displaystyle \sigma }$ is a list of terms in context ${\displaystyle \Gamma }$, one for each type in ${\displaystyle \Delta }$, having this type with the previous variables from ${\displaystyle \Delta }$ substituted by the previous terms in the list” (e.g., a parallel substitution from ${\displaystyle \Gamma }$ to ${\displaystyle x:A,y:B}$ in the syntax would be a term ${\displaystyle t}$ of type ${\displaystyle A}$ in context ${\displaystyle \Gamma }$ and a term ${\displaystyle u}$ of type ${\displaystyle B[x:=t]}$ in context ${\displaystyle \Gamma }$).

Let ${\displaystyle \operatorname {Fam} }$ denote the category of families of sets.^[a] An object of ${\displaystyle \operatorname {Fam} }$ is a family ${\displaystyle (A_{i})_{i\in I}}$ where ${\displaystyle I}$ is a set and each ${\displaystyle A_{i}}$ is a set. A morphism ${\displaystyle f:(A_{i})_{i\in I}\to (B_{j})_{j\in J}}$ in ${\displaystyle \operatorname {Fam} }$ is a function ${\displaystyle r:I\to J}$ together with, for each ${\displaystyle i\in I}$, a function ${\displaystyle t_{i}:A_{i}\to B_{r(i)}}$. (This category is equivalent to the arrow category of ${\displaystyle \operatorname {Set} }$, through the correspondence between a function ${\displaystyle f:A\to I}$ and the family of sets ${\displaystyle (f^{-1}(\{i\}))_{i\in I}}$.)

A category with families (CwF) consists of the following data:^[3][4][5][2]

• A category.

  The class of objects is denoted ${\displaystyle \operatorname {Con} }$ and the objects are called contexts. The class of morphisms from a context ${\displaystyle \Delta }$ to a context ${\displaystyle \Gamma }$ is denoted ${\displaystyle \operatorname {Sub} (\Delta ,\Gamma )}$ and these morphisms are called substitutions from ${\displaystyle \Delta }$ to ${\displaystyle \Gamma }$.

• A contravariant functor from this category to ${\displaystyle \operatorname {Fam} }$.

  The image of a context ${\displaystyle \Gamma }$ is a family of sets denoted ${\displaystyle (\operatorname {Tm} _{\Gamma }(A))_{A\in \operatorname {Ty} (\Gamma )}}$ (we usually drop the subscript in ${\displaystyle \operatorname {Tm} _{\Gamma }(A)}$). The elements of ${\displaystyle \operatorname {Ty} (\Gamma )}$ are called types in context ${\displaystyle \Gamma }$, and the elements of ${\displaystyle \operatorname {Tm} (A)}$ are called terms of type ${\displaystyle A}$ (in context ${\displaystyle \Gamma }$).

  The image of a substitution ${\displaystyle \sigma \in \operatorname {Sub} (\Delta ,\Gamma )}$ is a morphism ${\displaystyle (\operatorname {Tm} (A))_{A\in \operatorname {Ty} (\Gamma )}\to (\operatorname {Tm} (B))_{B\in \operatorname {Ty} (\Delta )}}$ in ${\displaystyle \operatorname {Fam} }$. Its component ${\displaystyle \operatorname {Ty} (\Gamma )\to \operatorname {Ty} (\Delta )}$ is denoted by ${\displaystyle A\mapsto A[\sigma ]}$, and for each ${\displaystyle A\in \operatorname {Ty} (\Gamma )}$, its component ${\displaystyle \operatorname {Tm} (A)\to \operatorname {Tm} (A[\sigma ])}$ is also denoted ${\displaystyle t\mapsto t[\sigma ]}$. These operations are respectively called substitution in types and substitution in terms.

  Alternatively, this data can be packaged as a presheaf of types ${\displaystyle \operatorname {Ty} }$ on the category of contexts, and a dependent presheaf of terms ${\displaystyle \operatorname {Tm} }$ on the category of contexts over the presheaf of types.

• A terminal object in the category of contexts.

  It is denoted ${\displaystyle \diamond }$ and called the empty context.

• For each context ${\displaystyle \Gamma }$ and for each type ${\displaystyle A\in \operatorname {Ty} (\Gamma )}$, consider the presheaf on the category of contexts which sends a context ${\displaystyle \Delta }$ to the set of pairs of a substitution ${\displaystyle \sigma \in \operatorname {Sub} (\Delta ,\Gamma )}$ and a term ${\displaystyle t\in \operatorname {Tm} _{\Delta }(A[\sigma ])}$. The functorial action of the presheaf on a substitution ${\displaystyle \delta \in \operatorname {Sub} (\Sigma ,\Delta )}$ is given by ${\displaystyle (\sigma ,t)\mapsto (\sigma \circ \delta ,t[\delta ])}$. The last part of the CwF data is a representing object for this presheaf, together with a natural isomorphism witnessing the representation.

  The representing context is denoted ${\displaystyle \Gamma \triangleright A}$ and called the context extension of ${\displaystyle \Gamma }$ by ${\displaystyle A}$.

  In one direction, the natural isomorphism sends a substitution ${\displaystyle \sigma \in \operatorname {Sub} (\Delta ,\Gamma )}$ and a term ${\displaystyle t\in \operatorname {Tm} (A[\sigma ])}$ to a new substitution ${\displaystyle (\sigma \triangleright t)\in \operatorname {Sub} (\Delta ,\Gamma \triangleright A)}$ called the substitution extension of ${\displaystyle \sigma }$ by ${\displaystyle t}$. In the other direction, it sends a substitution ${\displaystyle \sigma '\in \operatorname {Sub} (\Delta ,\Gamma \triangleright A)}$ to a pair of its tail ${\displaystyle \operatorname {tl} (\sigma ')\in \operatorname {Sub} (\Delta ,\Gamma )}$ and its head term ${\displaystyle \operatorname {hd} (\sigma ')\in \operatorname {Tm} (A[\operatorname {tl} (\sigma ')])}$.

  Explicitly, the fact that this is a natural isomorphism means that the following laws hold:$${\displaystyle {\begin{aligned}&\operatorname {tl} (\sigma \triangleright t)=\sigma \\&\operatorname {hd} (\sigma \triangleright t)=t\\&\sigma '=\operatorname {tl} (\sigma ')\triangleright \operatorname {hd} (\sigma ')\\&(\sigma \triangleright t)\circ \delta =(\sigma \circ \delta )\triangleright t[\delta ]\\&\operatorname {tl} (\sigma ')\circ \delta =\operatorname {tl} (\sigma '\circ \delta )\\&\operatorname {hd} (\sigma ')[\delta ]=\operatorname {hd} (\sigma '\circ \delta )\end{aligned}}}$$

Let ${\displaystyle \Gamma }$ be a context and ${\displaystyle A}$ a type in ${\displaystyle \Gamma }$. The head and tail of the identity substitution from ${\displaystyle \Gamma \triangleright A}$ to itself are respectively a substitution ${\displaystyle \operatorname {wk} \in \operatorname {Sub} (\Gamma \triangleright A,\Gamma )}$ called weakening, and a term ${\displaystyle \operatorname {vz} \in \operatorname {Tm} _{\Gamma \triangleright A}(A[\operatorname {wk} ])}$ called the head variable. Informally, the weakening adds an unused variable to the context, and the head variable is the term given by the variable last declared in the context.

Observe that weakening and the head variable allow to recover the tail and head of any substitution ${\displaystyle \sigma \in \operatorname {Sub} (\Delta ,\Gamma \triangleright A)}$ by $${\displaystyle \operatorname {tl} (\sigma )=\operatorname {tl} (\mathrm {id} \circ \sigma )=\operatorname {tl} (\mathrm {id} )\circ \sigma =\mathrm {wk} \circ \sigma }$$ and $${\displaystyle \operatorname {hd} (\sigma )=\operatorname {hd} (\operatorname {id} \circ \sigma )=\operatorname {hd} (\operatorname {id} )[\sigma ]=\operatorname {vz} [\sigma ].}$$

Furthermore, given a substitution ${\displaystyle \sigma \in \operatorname {Sub} (\Delta ,\Gamma )}$, and a type ${\displaystyle A\in \operatorname {Ty} (\Gamma )}$, we define a lifted substitution ${\displaystyle \sigma ^{+}\in \operatorname {Sub} (\Delta \triangleright A[\sigma ],\Gamma \triangleright A)}$ by ${\displaystyle \sigma ^{+}:=(\sigma \circ \mathrm {wk} )\triangleright \operatorname {vz} }$.

For each rule of a particular type theory, there is added structure and/or requirements on a CwF for it to model the type theory.

• A rule which introduces a type or term former is interpreted by an operation returning a type or term of the CwF, which is required to commute with substitution. The latter requirement is necessary since substitution is defined recursively in the syntax, e.g., ${\displaystyle (A\times B)[x:=t]}$ is ${\displaystyle A[x:=t]\times B[x:=t]}$.
• A rule adding definitional equalities is interpreted by a requirement that the operations on the CwF satisfy a corresponding equation.

To illustrate this, consider the case of dependent pair types (Σ-types). The type formation rule is

$${\displaystyle {\frac {\Gamma \ {\text{context}}\quad \Gamma \vdash A\ {\text{type}}\quad \Gamma ,x:A\vdash B\ {\text{type}}}{\Gamma \vdash (x:A)\times B\ {\text{type}}}}}$$

The corresponding operation on a CwF is: for each ${\displaystyle \Gamma \in \operatorname {Con} }$, for each ${\displaystyle A\in \operatorname {Ty} (\Gamma )}$, and for each ${\displaystyle B\in \operatorname {Ty} (\Gamma \triangleright A)}$, a type ${\displaystyle \Sigma (A,B)\in \operatorname {Ty} (\Gamma )}$. This operation is required to satisfy the substitution rule: for all substitution ${\displaystyle \sigma \in \operatorname {Sub} (\Delta ,\Gamma )}$ and types ${\displaystyle A\in \operatorname {Ty} (\Gamma ),B\in \operatorname {Ty} (\Gamma \triangleright A)}$, we must have ${\displaystyle \Sigma (A,B)[\sigma ]=\Sigma (A[\sigma ],B[\sigma ^{+}])}$.

The term formation rules for the pairing operation is:

$${\displaystyle {\frac {\Gamma \ {\text{context}}\quad \Gamma \vdash A\ {\text{type}}\quad \Gamma ,x:A\vdash B\ {\text{type}}\quad \Gamma \vdash t:A\quad \Gamma \vdash u:B[x:=t]}{\Gamma \vdash \langle t,u\rangle :(x:A)\times B}}}$$

The corresponding operation on a CwF is: for each ${\displaystyle \Gamma \in \operatorname {Con} }$, ${\displaystyle A\in \operatorname {Ty} (\Gamma )}$, ${\displaystyle B\in \operatorname {Ty} (\Gamma \triangleright A)}$, ${\displaystyle t\in \operatorname {Tm} (A)}$ and ${\displaystyle u\in \operatorname {Tm} (B[\operatorname {id} \triangleright t])}$), a term ${\displaystyle \langle t,u\rangle \in \operatorname {Tm} (\Sigma (A,B))}$. This must satisfy the substitution rule:

$${\displaystyle \langle t,u\rangle [\sigma ]=\langle t[\sigma ],u[\sigma ]\rangle .}$$

This equation is meaningful because of the CwF laws and the substitution rule for ${\displaystyle \Sigma }$. The left hand side is an element of ${\displaystyle \Sigma (A,B)[\sigma ]}$, which by the substitution rule for ${\displaystyle \Sigma }$ is equal to ${\displaystyle \Sigma (A[\sigma ],B[\sigma ^{+}])}$. To see that the right hand side is in this set, one has to check that ${\displaystyle u[\sigma ]}$ is in ${\displaystyle B[\sigma ^{+}][\operatorname {id} \triangleright t[\sigma ]]}$. This holds because ${\displaystyle u[\sigma ]}$ is in ${\displaystyle B[\operatorname {id} \triangleright t][\sigma ]}$ and

$${\displaystyle {\begin{aligned}&B[\operatorname {id} \triangleright t][\sigma ]\\&=B[(\operatorname {id} \triangleright t)\circ \sigma ]\\&=B[(\operatorname {id} \circ \sigma )\triangleright t[\sigma ]]\\&=B[\sigma \triangleright t[\sigma ]]\end{aligned}}}$$

while

$${\displaystyle {\begin{aligned}&B[\sigma ^{+}][\operatorname {id} \triangleright t[\sigma ]]\\&=B[(\sigma \circ \operatorname {wk} )\triangleright \operatorname {vz} ][\operatorname {id} \triangleright t[\sigma ]]\\&=B[((\sigma \circ \operatorname {wk} )\triangleright \operatorname {vz} )\circ (\operatorname {id} \triangleright t[\sigma ])]\\&=B[((\sigma \circ \operatorname {wk} )\circ (\operatorname {id} \triangleright t[\sigma ]))\triangleright \operatorname {vz} [\operatorname {id} \triangleright t[\sigma ]]]\\&=B[\sigma \circ (\operatorname {wk} \circ (\operatorname {id} \triangleright t[\sigma ]))\triangleright \operatorname {vz} [\operatorname {id} \triangleright t[\sigma ]]]\\&=B[\sigma \circ \operatorname {tl} (\operatorname {id} \triangleright t[\sigma ])\triangleright \operatorname {hd} (\operatorname {id} \triangleright t[\sigma ])]\\&=B[(\sigma \circ \operatorname {id} )\triangleright t[\sigma ]]\\&=B[\sigma \triangleright t[\sigma ]].\end{aligned}}}$$

Finally, the remaining rules for dependent pair types are the computation rules (or β-rules)

$${\displaystyle {\frac {\Gamma \ {\text{context}}\quad \Gamma \vdash A\ {\text{type}}\quad \Gamma ,x:A\vdash B\ {\text{type}}\quad \Gamma \vdash t:A\quad \Gamma \vdash u:B[x:=t]}{\Gamma \vdash \operatorname {fst} (\langle t,u\rangle )\equiv t:A}}}$$

$${\displaystyle {\frac {\Gamma \ {\text{context}}\quad \Gamma \vdash A\ {\text{type}}\quad \Gamma ,x:A\vdash B\ {\text{type}}\quad \Gamma \vdash t:A\quad \Gamma \vdash u:B[x:=t]}{\Gamma \vdash \operatorname {snd} (\langle t,u\rangle )\equiv u:B[x:=t]}}}$$

and the uniqueness rule (or η-rule)

$${\displaystyle {\frac {\Gamma \ {\text{context}}\quad \Gamma \vdash A\ {\text{type}}\quad \Gamma ,x:A\vdash B\ {\text{type}}\quad \Gamma \vdash p:(x:A)\times B}{\Gamma \vdash p\equiv \langle \operatorname {fst} (p),\operatorname {snd} (p)\rangle :(x:A)\times B}}}$$

These are interpreted by requiring the following equations on the previous operations:

• ${\displaystyle \operatorname {fst} (\langle t,u\rangle )=t}$ and ${\displaystyle \operatorname {snd} (\langle t,u\rangle )=u}$ (for ${\displaystyle \Gamma \in \operatorname {Con} }$, ${\displaystyle A\in \operatorname {Ty} (\Gamma )}$, ${\displaystyle B\in \operatorname {Ty} (\Gamma \triangleright A)}$, ${\displaystyle t\in \operatorname {Tm} (A)}$, ${\displaystyle u\in \operatorname {Tm} (B[\operatorname {id} \triangleright t])}$),
• ${\displaystyle p=\langle \operatorname {fst} (p),\operatorname {snd} (p)\rangle }$ (for ${\displaystyle \Gamma \in \operatorname {Con} }$, ${\displaystyle A\in \operatorname {Ty} (\Gamma )}$, ${\displaystyle B\in \operatorname {Ty} (\Gamma \triangleright A)}$, ${\displaystyle p\in \operatorname {Tm} (\Sigma (A,B))}$).

This section needs expansion with: mention how Russell and Coquand universes require stratifying the CwF, cite e.g. https://arxiv.org/abs/1902.08848. You can help by adding missing information. (November 2025)

The basic intuition stemming from the syntax is that a context is a list of types ${\displaystyle x_{0}:A_{0},\dots ,x_{k-1}:A_{k-1}}$, which is essentially equivalent to an iterated Σ-type ${\displaystyle (x_{0}:A_{0})\times \dots \times (x_{k-2}:A_{k-2})\times A_{k-1}}$. This is not true in all models, but it can be a useful property to consider.

A CwF is democratic when every context ${\displaystyle \Gamma }$ is isomorphic (in the category of contexts) to ${\displaystyle \diamond \triangleright A}$ for some closed type ${\displaystyle A}$ (i.e., a type in the empty context ${\displaystyle \diamond }$).^[6]: 6

The set model^{[4]: §3.5 [2]: 2 [3]: 24 [5]: §5}, or standard model, is the simplest model of type theory. Every construct is simply interpreted by its metatheoretic counterpart: a term of a function type is a function, a term of a product type is a pair, etc. (This is akin to the usual Tarskian semantics of first-order logic, and if one views type theory as a programming language, it is a metacircular interpreter.)

The CwF is defined as follows:

• A context is a set and a substitution is a function (so the category of contexts and substitutions is the category of sets).
• A type in ${\displaystyle \Gamma }$ is a family of sets ${\displaystyle (A_{i})_{i\in \Gamma }}$, and a term of this type is a choice of an element ${\displaystyle t_{i}\in A_{i}}$ for each ${\displaystyle i\in \Gamma }$. The action of a substitution ${\displaystyle \sigma :\Delta \to \Gamma }$ on a type ${\displaystyle (A_{i})_{i\in \Gamma }}$ gives ${\displaystyle (A_{\sigma (j)})_{j\in \Delta }}$, and on a term ${\displaystyle (t_{i}\in A_{i})_{i\in \Gamma }}$, it gives ${\displaystyle (t_{\sigma (j)}\in A_{\sigma (j)})_{j\in \Delta }}$.
• The empty context is a fixed singleton set.
• The extension of a context ${\displaystyle \Gamma }$ by a type ${\displaystyle (A_{i})_{i\in \Gamma }}$ is the type of pairs of an ${\displaystyle i\in \Gamma }$ and an element of ${\displaystyle A_{i}}$. The tail and head of a substitution ${\displaystyle \Delta \to (\Gamma \triangleright (A_{i})_{i\in \Gamma }),j\mapsto (i_{j},a_{j})}$ are given by ${\displaystyle j\mapsto i_{j}}$ and ${\displaystyle j\mapsto a_{j}}$.

All type formers are defined “pointwise”. For example, the product ${\displaystyle (A_{i})_{i\in \Gamma }\times (B_{i})_{i\in \Gamma }}$ is defined as ${\displaystyle (A_{i}\times B_{i})_{i\in \Gamma }}$, the pairing of terms ${\displaystyle (t_{i}\in A_{i})_{i\in \Gamma }}$ and ${\displaystyle (u_{i}\in B_{i})_{i\in \Gamma }}$ is ${\displaystyle ((t_{i},u_{i})\in A_{i}\times B_{i})_{i\in \Gamma }}$, etc. This model supports essentially any type former supported by the metatheory (with the exception of universes: the metatheory needs a stronger universe than the object theory contains, namely a universe large enough to contain all universes from the object theory, as is expected from Gödel's second incompleteness theorem). It can model the equality reflection rule of extensional type theory, but not univalence.

The syntactic model (or term model) is given by the contexts, parallel substitutions, types and terms in the syntax of the type theory under consideration, with the operations induced by all type and term constructors of the type theory.

For “reasonable” type theories, the syntactic model is also the initial model, which means that it has a unique morphism into every other model. The notion of morphism between models is usually defined by presenting the definition of a model as a generalized algebraic theory (GAT) (which is like an algebraic theory but allowing dependent functions), and applying the standard definition of morphism between algebras of a GAT. The initiality means that the syntax can indeed be interpreted in every model as expected. Actually establishing this turns out to be very tedious. While Cartmell and Hofmann proved it for some standard type theories, initiality became a contentious point in the research community around 2015 when some researchers, notably Voevodsky, opined that it was not justified to treat it as established for different type theories without carefully adapting the proofs. Most researchers consider the issue to have been satisfactorily solved by Uemura's introduction of the logical framework of second-order generalized algebraic theories (SOGATs), which encompasses practically all existing type theories (the main exception being substructural type theories), and his proof of initiality of the syntactic model for any SOGAT.^[7]

Meanwhile, it has also become common to eschew the traditional syntactic presentation of type theory entirely and define the syntax as the initial model (which exists for any GAT). This approach is called intrinsic syntax. At this level of abstraction, it is possible to construct and study models and to use type theory as an internal language for them (treating the traditional terms merely as a notation for elements of the model). It is not possible to study properties of the concrete, extrinsic syntax such as subject reduction and confluence. However, remarkably, the two main syntactic properties of some type theories, canonicity and normalization, can be stated and proved entirely at this level.^[8][9][10]

Let ${\displaystyle {\mathcal {C}}}$ be a category. The presheaf category ${\displaystyle {\hat {\mathcal {C}}}}$ is equipped with a canonical CwF structure as follows.^[3]: 45

A type ${\displaystyle A}$ in context ${\displaystyle \Gamma }$ is a dependent presheaf on ${\displaystyle {\mathcal {C}}}$ over ${\displaystyle \Gamma }$. This means the following data:

• For each object ${\displaystyle x\in {\mathcal {C}}}$, and for each element ${\displaystyle i\in \Gamma (x)}$, a set ${\displaystyle A(x,i)}$,
• For each morphism ${\displaystyle f:x\to y}$ in ${\displaystyle {\mathcal {C}}}$, and for each element ${\displaystyle i\in \Gamma (y)}$, a function ${\displaystyle A(f,i):A(y,i)\to A(x,\Gamma (f)(i))}$.

This data is subject to a functoriality requirement: ${\displaystyle A(g\circ f,i)=A(g,A(f)(i))\circ A(f,i)}$ and ${\displaystyle A(\operatorname {id} ,i)=\operatorname {id} }$.

Alternatively, ${\displaystyle A}$ can be viewed as a presheaf on the category of elements of ${\displaystyle \Gamma }$.

For a natural transformation ${\displaystyle \sigma :\Delta \to \Gamma }$, the substituted type ${\displaystyle A[\sigma ]}$ is defined by precomposition: it maps an object ${\displaystyle x\in {\mathcal {C}}}$ and an element ${\displaystyle i\in \Delta (x)}$ to ${\displaystyle A(x,\sigma _{x}(i))}$, and it maps a morphism ${\displaystyle f:x\to y}$ in ${\displaystyle {\mathcal {C}}}$ and an element ${\displaystyle i\in \Delta (x)}$ to the function ${\displaystyle A(f,\sigma _{x}(i))}$.

A term ${\displaystyle t}$ of type ${\displaystyle A}$ in context ${\displaystyle \Gamma }$ consists of, for each object ${\displaystyle x\in {\mathcal {C}}}$ and for each element ${\displaystyle i\in \Gamma (x)}$, an element ${\displaystyle t_{x}(i)\in A(x,i)}$, such that these choices are natural: for ${\displaystyle f:x\to y}$ in ${\displaystyle {\mathcal {C}}}$ and ${\displaystyle i\in \Gamma (y)}$, we should have ${\displaystyle t_{y}(\Gamma (f)(i))=A(f,i)(t_{x}(i))}$.

This section needs expansion with: rest of the CwF, and type formers, especially Π and universes. You can help by adding missing information. (June 2026)

This section needs expansion. You can help by adding missing information. (November 2025)

Other models of type theory include the setoid model,^{[citation needed]} the groupoid model,^[11] the simplicial set model,^[12] the assemblies model,^{[citation needed]} and several models in cubical sets starting with the BCH (Bezem–Coquand–Huber) model.^[13]

Traditional categorical logic involves correspondences between logics and kinds of categories which serve as their models. For example, elementary toposes are models of a form of intuitionistic higher-order logic, and regular categories are models of regular logic. The correspondence is used in both ways: a notion of model is fundamental to study a logic, e.g., to prove that a statement is unprovable by finding a model where it fails, and conversely, a category can be studied by reasoning in a logic of which it is a model, which is often called an internal language for the category.

For simple type theory, such correspondences can be found. For example, Cartesian closed categories model the simply typed λ-calculus with function, top and product types, and bicartesian closed categories model its extension with bottom and sum types. On the other hand, the situation is significantly more complicated for dependent type theory.

In the aforementioned semantics of simple type theory, a type is interpreted by an object of the category. In dependent type theory, a type depends on the value of the context in which it is defined, so one cannot simply use an object. Instead, a natural idea is to interpret a type ${\displaystyle A}$ in context ${\displaystyle \Gamma }$ by an object equipped with a morphism to the interpretation of ${\displaystyle \Gamma }$. The idea is to mimic the category of sets, where a family of sets ${\displaystyle (A_{i})_{i\in \Gamma }}$ can be represented categorically as the morphism ${\displaystyle r:A\to \Gamma }$, where ${\displaystyle A}$ is the disjoint union of all the ${\displaystyle A_{i}}$, which sends elements of each ${\displaystyle A_{i}}$ to their index ${\displaystyle i}$. The family ${\displaystyle (A_{i})}$ can be recovered by ${\displaystyle A_{i}=r^{-1}(i)}$.

This idea was used by Seely in a 1984 paper claiming that Martin–Löf type theory with Π types, Σ types and extensional identity types can be modelled in a locally Cartesian closed category (i.e., a category ${\displaystyle {\mathcal {C}}}$ such that all the slice categories ${\displaystyle {\mathcal {C}}/A}$ are Cartesian closed).^[14] However, it was later observed that Seely's proof is wrong. Substitution in types is modelled by pullback. For the interpretation of substitution to be sound, this operation must be strictly functorial way: pullback along ${\displaystyle g\circ f}$ must be exactly the same as pullback along ${\displaystyle f}$ followed by pullback along ${\displaystyle g}$. However, pullback involves an arbitrary choice and there is no reason for all these choices to be globally coherent: these pullbacks are always isomorphic, but have no reason to be the same. (Taking a skeleton of ${\displaystyle {\mathcal {C}}}$ does not help, since a pullback is not merely a choice of object but also a choice of morphisms.)

For example, call ${\displaystyle S:\mathbb {N} \to \mathbb {N} }$ the successor constructor of natural numbers, and consider the trivial proof that for a predicate ${\displaystyle P:\mathbb {N} \to {\mathcal {U}}}$, if ${\displaystyle P(0)}$ holds, ${\displaystyle P(1)}$ holds, and ${\displaystyle P(n)}$ holds for all ${\displaystyle n\geq 2}$ (call this hypothesis ${\displaystyle H}$), then ${\displaystyle P(n)}$ for all ${\displaystyle n}$. This is done by two inductions: the first reduces to proving ${\displaystyle (P(n))[n:=S(n')]}$ where ${\displaystyle n':\mathbb {N} }$ is a fresh variable, and the second reduces this to proving ${\displaystyle ((P(n)[n:=S(n')])[n':=S(n'')]}$ where ${\displaystyle n'':\mathbb {N} }$ is fresh. By applying the hypothesis ${\displaystyle H}$ to ${\displaystyle S(S(n''))}$ (noting that ${\displaystyle S(S(n''))\geq 2}$), one obtains an element of ${\displaystyle (P(n))[n:=S(S(n''))]}$. This only works because in the syntax of type theory, the substituted types ${\displaystyle (P(n))[n:=S(S(n''))]}$ and ${\displaystyle ((P(n))[n:=S(n')])[n':=S(n'')]}$ are the same, namely ${\displaystyle P(S(S(n''))}$. On the other hand, using the interpretation of substitution as pullback, the interpretations of these two types would only be isomorphic and it would not be semantically justified to use elements of one as elements of the other.

The same problem arises with the interpretation of type formers, which must commute with substitution, whereas this fails in Seely's purported model. For example, given a dependent function ${\displaystyle f:(x:A)\to (P(x)\times Q(x))}$, the application ${\displaystyle f(g(y))}$ has type ${\displaystyle (P(x)\times Q(x))[x:=g(y)]}$. Without an actual equality between this type and ${\displaystyle P(g(y))\times Q(g(y))}$, it is not semantically justified to apply the first projection to ${\displaystyle f(g(y))}$ to obtain an element of ${\displaystyle P(g(y))}$.

For this reason, type theory is not modelled directly in categories with properties, but rather in categories enriched with structure, such as CwFs, which include a set of types for each context and a substitution operation on types required to be functorial. The usual way to define a model is to start from a category with good enough properties and define this structure analogously to categorical constructions, but taking care to preserve coherence. This process is sometimes referred to as strictification.

There are several strictification constructions for doing this in general. A construction due to Bénabou was used by Hofmann to interpret MLTT in any locally Cartesian closed category, thus repairing Seely's result (with a different semantic interpretation).^[15][6] More recently, Lumsdaine and Warren proposed the local universes construction, which delays computing pullbacks by modelling a type in ${\displaystyle \Gamma }$ as two objects ${\displaystyle U}$ and ${\displaystyle A}$ with a pair of morphisms ${\displaystyle \Gamma \to U\leftarrow A}$, so that applying a substitution ${\displaystyle \Delta \to \Gamma }$ can be simply performed by composition of ${\displaystyle \Delta \to \Gamma }$ with ${\displaystyle \Gamma \to U}$, which is functorial.^{[16][4]: §6.5.5}

However, in most concrete cases, the strictification can be done by hand, and the result is simpler to work with than the output of such general constructions. For example, in the set model, types in context ${\displaystyle \Gamma }$ are defined as the actual families of sets ${\displaystyle (A_{i})_{i\in \Gamma }}$ rather than a functions ${\displaystyle A\to \Gamma }$ so that the application of a substitution ${\displaystyle \gamma :\Delta \to \Gamma }$ can simply be the family ${\displaystyle (A_{\gamma (j)})_{j\in J}}$. This definition of substitution is strictly functorial, unlike pullback in the category of sets. The presheaf model is another typical example: substitution is made functorial by replacing presheaves ${\displaystyle A}$ with a natural transformation to ${\displaystyle \Gamma }$ by dependent presheaves over ${\displaystyle \Gamma }$.